By Christian Findlay 28 Jul 2026

Type System

• Hindley-Milner Inference
• Generics and Variance
• Built-in Types
• Result Preservation
• Function Types
• Record Types
• Union Types
• Collection Types
• Built-in Error Types
• The any Type
• Type Annotations

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) -> Result<int, MathError>
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) -> Result<int, MathError>
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] (Error Handling): integer + - * return Result<int, MathError>. With a float operand, the integer is promoted and the IEEE-754 operation returns plain float.

Annotations are optional where inference has enough context. 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>

Record Type Unification

Two record types unify iff they have the same set of field names and corresponding field types unify. Field order is irrelevant in both declaration and construction.

unify(R1, R2) :=
    if names(R1) ≠ names(R2) then FAIL
    else for each f ∈ names(R1): unify(typeOf(R1, f), typeOf(R2, f))

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.

[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.

[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.

Mixed numeric arithmetic promotes int to float. Integer +, -, *, and unary - return Result<int, MathError>; / and % return Result<_, MathError>. Floating-point +, -, *, and unary - return plain float (ARITH-CHECKED).

Result Preservation

A fallible expression has type Result<T, E>, and the compiler never implicitly erases that wrapper. Passing it to a function or concurrency operation that expects T, assigning it to a plain T cell or annotation, returning it from a function declared to return T, comparing it with a T, or using it through a function value is a type error. Interpolation and formatting preserve and display the complete Success or Error value.

Callers obtain the success payload only through an exhaustive match or an explicit ?: fallback. The sole compositional exception is failure-preserving arithmetic chaining: compatible numeric Result<T, MathError> operands propagate the first error and flatten the chain to one Result<T, MathError> (Chaining Arithmetic). It never turns the chain into a plain number.

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) -> Result<int, MathError> = fn(x: int) => x * 2

fn createAdder(n: int) -> (int) -> Result<int, MathError> = fn(x: int) => x + n

applyFunction : (int, (int) -> int) -> int
applyFunction (value, transform) = transform value

doubler : int -> Result<int, MathError>
doubler = \x => x * 2

createAdder : int -> int -> Result<int, MathError>
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) -> Result<int, MathError> = 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) -> Result<int, MathError>
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

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

Direct field access is permitted only on a record value. A Result or union must be matched to a concrete payload before field access. Because any has no runtime type tag, it cannot be narrowed for field access.

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) ?: 0
}

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) ?: 0

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

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")

any does not carry a runtime type tag and does not provide dynamic type tests. Code that consumes its representation must already know what was passed. It is used mainly at heterogeneous builtin and foreign-function boundaries. In particular, print and toString cannot recover an aggregate hidden behind any; they render its raw pointer-sized representation rather than its fields.

Type Annotations

An annotation constrains inference and is checked against the expression:

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).