By Christian Findlay

Type System

Hindley-Milner Inference

Osprey uses Hindley-Milner inference over the canonical AST produced by either surface syntax ([FLAVOR-BOUNDARY]). Examples show both surfaces where their spellings differ.

Type annotations are optional everywhere they can be inferred:

fn identity(x)         = x                       // <T>(T) -> T
fn add(a, b)           = a + b                   // (int, int) -> int
fn greet(name)         = "Hello, " + name        // (string) -> string
fn makeUser(n, a)      = User { name: n, age: a }  // (string, int) -> User
fn getName(u)          = u.name                  // (User) -> string
fn twice(f, x)         = f(f(x))                 // <T>((T) -> T, T) -> T
fn compose(f, g)       = fn(x) => f(g(x))        // <A,B,C>((B)->C,(A)->B) -> (A)->C
identity x       = x                        // <T>(T) -> T
add (a, b)       = a + b                     // (int, int) -> int
greet name       = "Hello, " + name          // (string) -> string
makeUser (n, a)  =
    User
        name = n
        age = a                             // (string, int) -> User
getName u        = u.name                    // (User) -> string
twice (f, x)     = f (f x)                   // <T>((T) -> T, T) -> T
compose (f, g)   = \x => f (g x)             // <A,B,C>((B)->C,(A)->B) -> (A)->C

add follows ARITH-CHECKED: integer + - * return int. With a float operand, the integer is promoted and the IEEE-754 operation returns plain float.

Record fields and foreign declarations include types as part of their syntax; annotations on bindings and functions constrain the inferred type.

A polymorphic function is monomorphised independently at each call site:

let i = identity(42)        // identity<int>
let s = identity("hello")   // identity<string>
i = identity 42          // identity<int>
s = identity "hello"     // identity<string>

Reporting a Partly Inferred Type — [TYPE-RENDER-HOLES]

Inference does not always reach a single ground type, and what a tool reports in that case is part of the language's contract. A slot the checker proved nothing about is written _, the type-level hole. Every slot it did prove is written normally, so a partial answer still carries its proven part.

fn bothArms(f) = if f { Success { value: 1 } } else { Error { message: "e" } }
// reported: fn bothArms(f: bool) -> Result<int, _>

Reporting is a property of the canonical AST, so both surfaces report the same signature for the same program ([FLAVOR-IR-EQUIV]).

The payload is int in both arms, so it is reported. The error side is open: Error { message } fixes only the message, leaving E free to unify with whichever error type a call site supplies, so -> Result<int, string>, -> Result<int, Error> and -> int all check (Result Preservation). A hole is the only honest spelling for that slot.

A declared record is reported by its name and its row together:

type Box<T> = { value: T }
fn boxed() = Box { value: 1 }
// reported: fn boxed() -> Box { value: int }

Either half alone loses something. The row alone drops the name its author wrote — and for a record declared with type, the row is not even an annotation they may write back. The name alone drops the instantiation: a record carries no type arguments, so Box<int> cannot be reconstructed from Box, and the int the checker proved simply disappears. Saying both costs nothing.

Two spellings are forbidden. A tool must not print the checker's internal variable name — t5 is private, its number is an artefact of one inference run and it moves when an unrelated line is edited. A tool must not substitute Unit, which is a positive claim the checker itself refutes: annotating bothArms with -> Unit fails to unify. Where a type is nothing but a hole there is nothing to report, and the slot is left as the author wrote it — bare — rather than decorated with _.

A hole is a reporting spelling, not syntax. The annotation grammar has no wildcard, so _ written in a type position is read as an ordinary nominal name like any other capitalized-or-not identifier, and it unifies only where the slot was already free. -> Result<int, _> therefore happens to check on bothArms, while fn f(x: int) -> _ = x is rejected — cannot unify _ with int — exactly as a misspelled type name would be. A reported signature containing a hole is not guaranteed to be a valid annotation, and reporting one is not a suggestion to write it down: an annotation the checker can prove adds no information and is redundant (Type Annotations).

Rows and Record Type Unification — [TYPE-ROW]

A row is an unordered set of name: type fields. It is the one structure behind every product in the language: a named record, an anonymous record, a tuple, and a union variant's payload are all rows, and they unify by the same rule. Field order is irrelevant in declaration, construction and matching.

A row is closed (it has exactly these fields) or open (it has at least these fields, written ..). Two closed rows unify iff they carry the same field names and each corresponding field type unifies. An open row unifies with any row that carries its named fields.

unify(R1, R2) :=
    if closed(R1) and closed(R2) and names(R1) ≠ names(R2) then FAIL
    if open(R1) and names(R1) ⊄ names(R2) then FAIL
    else for each f ∈ names(R1) ∩ names(R2): unify(typeOf(R1, f), typeOf(R2, f))

Open rows appear only in patterns (Structural patterns) and in any narrowing (TYPE-ANY). A declared type is always closed.

Status: closed-row unification is implemented and is what makes two identically-shaped records interchangeable today. Open rows exist exactly where this section places them — a ..-opened structural pattern and any narrowing — and nowhere in type annotations.

Polymorphic Variables vs any

Inference produces polymorphic variables (<T>, <A>, …), not any. The any type is opt-in; see The any Type.

Generics and Variance

Flavor layer — shared core. Both surfaces lower to the same variance-carrying TypeParam nodes ([FLAVOR-BOUNDARY]); the ML spellings are specified in ML Flavor Syntax.

[TYPE-GENERICS-DECL] Type declarations bind type parameters; constructions may pin them explicitly. type Pair<T, U> = … binds T/U across every variant field. A construction site may apply explicit type arguments — Pair<int, string> { first: 1, second: "a" } — which unify with the instantiation the fields would otherwise infer; an argument that contradicts a field is a type error.

[GENERICS-CTOR-ARITY] Explicit constructor type arguments must match the declaration's arity. Box<int> { v: 1 } against type Box<T> is well-formed; Box<int, string> { v: 1 } is rejected with takes 1 type argument(s), got 2. Writing the arguments out is a contract with the declaration, so a count mismatch is an error rather than a silently ignored annotation.

[TYPE-GENERICS-FN] Functions bind type parameters with fn name<T, …>. A binder makes every use of T in the signature the SAME inference variable; without it, T in an annotation names a nominal type. The binder is load-bearing exactly when a parameter must relate two or more positions (fn pick<T>(first: T, second: T) pins both arguments to one type) or when a caller must pin an otherwise-unconstrained variable. HM inference is unchanged: unannotated functions stay implicitly polymorphic, and a polymorphic function is monomorphised independently at each call site. Variance markers are not permitted on function binders (variance is declaration-site on types and effects only — [TYPE-VARIANCE-DECL]).

fn pick<T>(first: T, second: T) = first
let n = pick(10, 20)
let s = pick("left", "right")
pick<T> : (T, T) -> T
pick (first, second) = first
n = pick (10, 20)
s = pick ("left", "right")

In the ML flavor the binder lives on the signature line (pick<T> : …); a binding without a signature cannot declare type parameters.

A generic function used as a VALUE is specialised wherever its ABI can be fixed: by a consuming slot, by a call alias, or — when a generic function returns a lambda — at each call site of the binding, which is inlined and specialised there. fn pick() = |x| => x followed by let f = pick() therefore serves f(7), f("os") and f(2.5) from one binding. A lambda so returned may close over the producing call's parameters (fn constly(v) = |x| => v); those are evaluated once, at the binding, so the call's effects happen as often as the source performs it, not once per instantiation.

One shape has no ABI to fix and is rejected rather than guessed: a still-generic lambda used as a bare value, with no call site to specialise against — print("${mk(1)}") for fn mk(x) = |y| => x. The compiler answers a closure value with a still-generic type. This is a permanent restriction, not a missing feature: one runtime closure has one representation, and lowering an unresolved type variable as a machine word would read a string or float instantiation as an integer.

[TYPE-VARIANCE-DECL] Type parameters declare variance at the declaration site: out T (covariant — T only flows out), in T (contravariant — T only flows in), unannotated (invariant — exact match). out and in are contextual keywords, reserved only inside type-parameter lists (Lexical Structure).

type Feed<out T> = Feed { supply: T } | Dry
type Gate<in T>  = Gate { admit: (T) -> bool } | Open
type Feed out T =
    Feed
        supply : T
    Dry
type Gate in T =
    Gate
        admit : T -> bool
    Open

[TYPE-VARIANCE-POSITIONS] Variance is position-checked. Walking a declaration's field (or effect-operation) types: fields and function results are OUTPUT positions; function parameters flip the polarity (INPUT); a nested constructor's argument composes the position with that constructor's declared variance (an invariant argument position demands both directions, so only invariant parameters may sit there). A covariant parameter in an input position, or a contravariant parameter in an output position, is a compile error. Effect operations check the same way: operation parameters are inputs, operation results outputs (Algebraic Effects).

[TYPE-VARIANCE-ASSIGN] Variance directs assignability structurally, and the leaves match exactly. Plain HM unification is untouched — every well-typed expression keeps a principal type. At assignment sites (call arguments, annotated bindings, return positions), a variance-declared constructor's arguments are matched directionally: covariant (out) arguments recurse expected-accepts-actual, contravariant (in) arguments recurse with the roles flipped, invariant arguments unify exactly. The recursion continues only through variance-declared constructors and bottoms out in exact unification. There is no Result<T, E>-to-T coercion at any depth or direct value site: it would erase a failure and accept a value with the wrong representation. Function returns also match exactly, so a Feed<(int) -> Result<int, Error>> does not match a Feed<(int) -> int> slot.

Built-in constructors' declared variance: Result<out T, out E>, List<out T>, Fiber<out T>, Map<K, out V> (keys invariant); Channel<T> and Ptr are invariant. Function types are structurally contravariant in parameters and covariant in returns.

Built-in Types

Primitive spellings are case-sensitive.

Type Description
int 64-bit signed integer (LLVM i64)
float 64-bit IEEE 754 (LLVM double)
string UTF-8 encoded
bool true | false
Unit The single value (); the return type of a function with no result
any Erased compatibility value; no runtime type tests
Result<T, E> Error-handling sum type (see Error Handling)
List<T> Immutable sequential collection
Map<K, V> Immutable key/value collection
Iterator<T> Opaque range pipeline (see Iterators)

Mixed numeric arithmetic promotes int to float. Integer +, -, *, %, and unary - have type int; / has type float; floating-point +, -, *, and unary - have type float. Arithmetic is total: no trap, no panic, no silent wrap, no unspecified value, and no undischarged fault (ARITH-CHECKED, ARITH-TOTAL).

Result Preservation

A fallible expression has type Result<T, E>, and the compiler never implicitly erases that wrapper (FAILURE-EXPLICIT). Every consuming position — arguments, bindings, plain-T returns, comparisons, function-value calls — preserves the Result or is rejected; interpolation displays the complete Success or Error value. Callers obtain the payload only through an exhaustive match or an explicit ?: fallback. This rule has no exceptions. Arithmetic is not one: it carries no Result wrapper at all, and its faults are discharged by an Arith handler rather than by erasing a wrapper (ARITH-TOTAL).

Function Types

functionType ::= "(" (type ("," type)*)? ")" "->" type
(int) -> int
(int, string) -> bool
() -> string
(string) -> (int) -> bool          // higher-order
fn applyFunction(value: int, transform: (int) -> int) -> int = transform(value)

let doubler: (int) -> int = fn(x: int) => x * 2

fn createAdder(n: int) -> (int) -> int = fn(x: int) => x + n
applyFunction : (int, (int) -> int) -> int
applyFunction (value, transform) = transform value

doubler : int -> int
doubler = \x => x * 2

createAdder : int -> int -> int
createAdder n = \x => x + n

Multi-argument call syntax (named arguments are required for two or more parameters) is in Function Calls.

Closures — [TYPE-FN-CLOSURE]

A lambda (fn(...) => expr or |x| => expr) captures every free identifier from its enclosing lexical scope by reference to its value at capture time. Captured bindings are immutable, so by-reference and by-value capture are observationally identical and the implementation MAY choose either. A captured binding outlives the surrounding stack frame: a closure returned from a function remains callable and continues to read the captured values.

fn makeAdder(n: int) -> (int) -> int = fn(x: int) => x + n

let add5    = makeAdder(5)
let add10   = makeAdder(10)
print(add5(3))     // Success(8)
print(add10(3))    // Success(13)

let prefix  = "hello "
let greet   = fn(name: string) => prefix + name              // captures prefix
print(greet("world"))                                         // "hello world"
makeAdder : int -> (int) -> int
makeAdder n = \(x : int) => x + n               // captures n

add5    = makeAdder 5
add10   = makeAdder 10
print (add5 3)     // Success(8)
print (add10 3)    // Success(13)

prefix  = "hello "
greet   = \(name : string) => prefix + name     // captures prefix
print (greet "world")                                         // "hello world"

Closures and named functions are interchangeable wherever their complete function types match, including iterator callbacks and record fields. A Result<T, E> returned through a function-value call remains a Result<T, E> and must be handled explicitly (Result Preservation).

Higher-order calls — [TYPE-FN-HIGHER-ORDER]

Any expression with a function type is callable. The callee may be a local, record field, returned closure, or another call expression; it need not be a top-level function name. Chained application evaluates one function result per call, so makeAdder(1)(2) calls the closure returned by makeAdder(1).

Record Types

recordType ::= "type" ID "=" "{" field ("," field)* "}" constraint?
field      ::= ID ":" type
constraint ::= "where" function_name
type Point   = { x: int, y: int }
type Person  = { name: string, age: int, active: bool }
type Point =
    x : int
    y : int

type Person =
    name : string
    age : int
    active : bool

Anonymous Records — [TYPE-RECORD-ANON]

A row written without a type declaration is an anonymous record. The type spelling is the declaration's right-hand side, and the value spelling is the construction form without a head:

fn describe(p: { x: int, y: int }) -> string = "${p.x},${p.y}"

let origin = { x: 0, y: 0 }

An anonymous record unifies with a declared record of the same row (TYPE-ROW), so origin is accepted wherever a Point is expected. Field keys are bare identifiers; that is what separates a record from a map literal, whose keys are string or expression values ({ "Dave": 28 }). A brace literal with no fields is the empty map, not the empty record.

Tuples — [TYPE-TUPLE]

A tuple is a row whose field names are the decimal positions 0, 1, …, the same encoding a positionally-declared union payload already uses (TYPE-UNION-POSITIONAL):

A positionally-declared union payload IS such a row, and is what a tuple pattern reads today — the standalone (1, "a") value and its (int, string) type spelling do not parse yet (see the status note below):

type Pair = Pair(int, string)

let described = match erased {
    (n, label) => "${label}=${n}"
    _          => "unknown"
}

A decimal string is not a valid identifier in either flavor, so a tuple field cannot be named in source — pair.0 does not parse. Tuples are read by pattern matching (Tuple patterns), which keeps them consistent with the rule that unions and any are read by matching rather than by projection.

A one-element parenthesis is grouping, never a tuple: (x) is x.

Status: anonymous record values construct, project fields and match structurally, but cannot be erased into any — narrowing selects among DECLARED rows, so let v: any = { x: 1 } is rejected with declare its row as a named type first. Tuple patterns are implemented in both flavors as the positional row spelling; tuple values and the (int, string) type spelling are not, so a tuple pattern today selects a positionally-declared record (type Pair = Pair(int, string)), plain or erased.

Construction

let point  = Point  { x: 10, y: 20 }
let person = Person { name: "Alice", age: 30, active: true }

// Field order at construction is irrelevant
let person2 = Person { active: true, name: "Bob", age: 22 }
point =
    Point
        x = 10
        y = 20
person =
    Person
        name = "Alice"
        age = 30
        active = true

// Field order at construction is irrelevant
person2 =
    Person
        active = true
        name = "Bob"
        age = 22

All fields are required. Missing or unknown fields, or type mismatches, are compilation errors.

Field Access — [TYPE-FIELD-ACCESS-NON-RECORD]

Direct field access is permitted only on a record value. A Result, a union or an any must be matched to a concrete payload or row before field access (TYPE-ANY).

Field access on a type that can never carry fields — int, float, string, bool, Unit — is rejected by the type checker with cannot access field '<field>' on non-struct type <type>, naming the offending source line. The check is deliberately narrow: any unifies with records, a collection's element may be a record, and an unresolved type variable may still infer to one, so none of those are rejected here. Without the check, codegen emitted invalid LLVM and the failure surfaced from clang against a temporary .ll file instead of the user's source.

let n = person.name        // ok

// Result: match before access
match personResult {
    Success { value }   => print(value.name)
    Error   { message } => print(message)
}

// Union: discriminate first
let area = match shape {
    Circle    { radius }         => 3.14 * radius * radius
    Rectangle { width, height }  => width * height
}
n = person.name        // ok

// Result: match before access
match personResult
    Success value => print value.name
    Error message => print message

// Union: discriminate first
area =
    match shape
        Circle radius => 3.14 * radius * radius
        Rectangle width height => width * height

Codegen resolves a named-field payload by name, never by declaration order, so reordering fields in a type cannot silently rebind a pattern. A positionally-declared variant (TYPE-UNION-POSITIONAL) has no field names to resolve against and is the one case resolved by index — the binder in column i binds payload slot i.

Immutability and Non-Destructive Update

Records cannot be modified. To produce a record that differs in some fields from an existing one, use the update form:

let p2 = point  { x: 15 }                // y carried over
let p3 = person { age: 26, active: false }
p2 = point(x = 15)               // y carried over
p3 = person(age = 26, active = false)

Nested Records

type Address = { street: string, city: string, zipCode: string }
type Company = { name: string, address: Address }

let company = Company {
    name:    "Tech Corp",
    address: Address { street: "456 Tech Ave", city: "Sydney", zipCode: "2000" }
}

let companyCity = company.address.city
type Address =
    street : string
    city : string
    zipCode : string

type Company =
    name : string
    address : Address

company = Company(name = "Tech Corp", address = Address(street = "456 Tech Ave", city = "Sydney", zipCode = "2000"))

companyCity = company.address.city

Union Types

A union type (also "sum type", "tagged union", "discriminated union") declares a closed set of named variants. Each variant is nullary (no payload), carries a record-style named payload, or carries a positional payload (TYPE-UNION-POSITIONAL). Grammar in Syntax; pattern-matching rules in Pattern Matching.

type Color  = Red | Green | Blue
type Shape  = Circle    { radius: float }
            | Rectangle { width:  float, height: float }
            | Triangle  { a: float, b: float, c: float }
type Color =
    Red
    Green
    Blue

type Shape =
    Circle
        radius : float
    Rectangle
        width : float
        height : float
    Triangle
        a : float
        b : float
        c : float

A union value carries a runtime discriminant identifying its variant; the compiler emits one branch per variant in any match. Field access on a union requires match to narrow it to a single variant first.

Recursive Variants — [TYPE-UNION-REC]

A variant's payload MAY reference the union type itself, either directly or through a built-in collection. Recursive payloads represent trees such as ASTs, file trees, scene graphs, and parsed JSON.

type Tree = Leaf | Node { value: int, left: Tree, right: Tree }

type JsonValue =
    JNull
    | JBool { v: bool }
    | JNum  { v: float }
    | JStr  { v: string }
    | JArr  { items:   List<JsonValue> }
    | JObj  { entries: Map<string, JsonValue> }
type Tree =
    Leaf
    Node
        value : int
        left : Tree
        right : Tree

type JsonValue =
    JNull
    JBool
        v : bool
    JNum
        v : float
    JStr
        v : string
    JArr
        items : List<JsonValue>
    JObj
        entries : Map<string, JsonValue>

A recursive union is laid out indirectly — variant payloads referencing the same type, or containing a List<Self> / Map<K, Self>, MUST be stored behind a pointer so the type's size is finite. Construction, pattern-matching, and field access use the same syntax as other variants. Mutually recursive unions follow the same rule.

Collection Types

List<T> and Map<K, V> are immutable runtime collections. Collection operations return a new value and leave their inputs unchanged. Their builtin signatures are listed in Built-in Functions.

List<T> — [TYPE-LIST]

List<T> is a homogeneous indexed sequence. Index access is bounds-checked and returns Result<T, Error>.

let numbers = [1, 2, 3, 4, 5]            // List<int>
let names   = ["Alice", "Bob"]           // List<string>

// Empty literal cannot infer its element type unless the context provides it
let empty: List<int> = []                // ok
let total = sumOfInts([])                // ok if sumOfInts: (List<int>) -> int

match numbers[0] {
    Success { value }   => print(value)
    Error   { message } => print(message)
}

Operations — [TYPE-LIST-OPS]

let withSix  = listAppend(numbers, 6)
let reversed = listReverse(numbers)
let combined = numbers + [6, 7, 8]
forEachList(numbers, fn(x) => print(toString(x)))

+ is equivalent to listConcat. listAppend, listPrepend, listReverse, and concatenation return new lists.

Patterns — [TYPE-LIST-PATTERNS]

fn classify(xs: List<int>) -> string = match xs {
    []                 => "empty"
    [single]           => "one"
    [first, second]    => "two"
    [head, ...tail]    => "many starting with ${head}"
}

A list pattern matches exactly the listed length unless its final element is a rest binder (...name). The rest binder receives the remaining List<T>.

Map<K, V> — [TYPE-MAP]

Map<K, V> is an associative collection. The constructors and map literals create string-keyed maps, so their concrete public type is Map<string, V>. Iteration order is unspecified.

Literals — [TYPE-MAP-LITERAL]

let ages = {
    "Alice":   25,
    "Bob":     30,
    "Charlie": 35
}                                                 // Map<string, int>

The ML spelling is ["Alice" => 25, "Bob" => 30]. Use Map() in Default syntax or [=>] in ML syntax for an empty map.

let scores = Map()

Entries are inserted left to right; the last value wins when a literal repeats a key.

Lookup — [TYPE-MAP-LOOKUP]

Index lookup returns Result<V, Error>:

match ages["Alice"] {
    Success { value }   => print(toString(value))
    Error   { message } => print(message)
}

Operations — [TYPE-MAP-OPS]

All operations return a new map and never mutate the receiver.

let updated    = mapSet(ages, "Alice", 26)
let withoutBob = mapRemove(ages, "Bob")
let merged     = ages + { "Dave": 28 }
let names      = mapKeys(ages)
let values     = mapValues(ages)

mapMerge and map + are right-biased: the right map wins on duplicate keys.

Built-in Error Types

Type Used by
Error Fallible builtins, including parsing, checkedAdd/checkedSub/checkedMul, collection lookup, files, and processes

Success and Error are the constructors of Result<T, E> (see Error Handling).

The any Type — [TYPE-ANY]

any is an erased compatibility type. It unifies with every other type, so an any parameter accepts values of different static types:

fn ignore(value: any) -> string = "ignored"

let a = ignore(42)
let b = ignore("text")

Erasure keeps the value's row (TYPE-ROW), so an any is narrowed back to a usable type by matching its structure — never by an unchecked cast:

let described = match value {
    { message, .. } => message
    { code, .. }    => "code ${code}"
    _               => "unknown"
}

Structural narrowing is the only way to read a field of an any. An arm naming a field the value does not carry does not select, so recovery can never read a word that was never a pointer, and a match over any is never exhaustive — it requires a catch-all (TYPE-MATCH-EXHAUSTIVE).

Erasing an int, float or bool keeps a scalar row: those values carry no fields, so every field-naming arm declines and only a binding or _ arm selects them.

Status: implemented. An erased value is a pointer to a two-word box { desc, payload } whose descriptor names its runtime shape, on every memory backend and both flavors. The one-way rule holds at annotations (cannot recover … from an erased any``), and every other read of the raw word is rejected too: operators (erased() == x, x + 1), field access, indexing, and the pattern forms that carry no row test — literal, list, variant and type-annotated arms. Structural narrowing selects among the DECLARED record rows by descriptor identity, so an erased record made by any constructor with the same field names matches the same arm; a field bound from a narrowing is itself any until matched further. print/toString render through the descriptor: scalars and strings exactly, records as their row ({ x: 1, y: 2 }), unions by variant, a Result as Success(…)/Error(…), and shapes rendering cannot see into — lists, maps, closures, foreign handles — as a named placeholder such as <list>, never the raw word. Erasing an anonymous record is rejected (TYPE-RECORD-ANON); a structural arm never selects an erased union, list or map — match the union before erasing it.

Type Annotations — [TYPE-ANNOTATION-CHECK]

An annotation constrains inference and is checked against the expression. A primitive spelling is case-sensitive, so Int is not int: an unknown capitalized name is a nominal type, and assigning an int to a variable annotated Int is a type mismatch rather than a silent alias.

let xs: List<int> = []
fn half(n: int) -> Result<int, Error> = intDiv(n, 2)

Writing -> int for half would be a type error; a return annotation cannot erase the body's Result (Result Preservation).