Examples

The integration tests for the row-poly crate are organised as a sequence of .fun source files paired with insta snapshots that pin the printed types. Each section below walks through one of those files and explains what the type system is doing on the inputs. The full source of each file is included inline so the prose and the inputs cannot drift apart.

Basics

The simplest programs construct records, read fields, and build records inside lambdas. Every constructor and selector lines up directly with one of the inference rules from the Implementation chapter.

#![allow(unused)]
fn main() {
Basic record construction and selection.

The empty record.
{}

A single field.
{x = 1}

Multiple fields, mixed types.
{x = 1, y = true, z = false}

Nested records.
{a = {b = 1}}
{a = {b = {c = 42}}}

Chained selection.
{a = {b = 1}}.a
{a = {b = 1}}.a.b
{a = {b = {c = 42}}}.a.b.c

Records inside a lambda body.
\x -> {self = x}
\x -> \y -> {a = x, b = y}

Record let-binding then selection.
let p = {x = 1, y = 2} in p.x
let p = {x = 1, y = 2} in p.y

Record fields holding functions.
{id = \x -> x}
{add = \x -> \y -> x, sub = \x -> \y -> y}
}

The empty record {} infers as {}, the record type wrapping the closed empty row. A literal {x = 1, y = true, z = false} infers as {x : Int, y : Bool, z : Bool} because record extension prepends each field’s inferred type onto the row. Nested records nest in the obvious way: {a = {b = 1}} has type {a : {b : Int}}, and chained selection like {a = {b = 1}}.a.b projects through both layers to recover Int. The lambdas demonstrate that a record literal in a function body refers to its parameters by their fresh type variables, so \x -> \y -> {a = x, b = y} is principal at a -> b -> {a : a, b : b}.

Scoped Labels

Scoped labels are the feature that distinguishes this calculus from a set-of-labels presentation. Duplicate labels are allowed and behave like a stack, with selection and restriction always operating on the leftmost occurrence.

#![allow(unused)]
fn main() {
Duplicate labels are allowed and form a stack.
Selection and restriction always operate on the leftmost occurrence.

Duplicate label, same type.
{x = 1, x = 2}

Duplicate label, different types.
{x = 1, x = true}

Three-deep stack.
{x = 1, x = true, x = false}

Selection picks the leftmost.
{x = 1, x = true}.x
{x = true, x = 1}.x
{x = 1, x = true, x = false}.x

Restriction peels off the leftmost, exposing the next.
{{x = 1, x = true} - x}.x
{{x = true, x = 1} - x}.x
{{{x = 1, x = true, x = false} - x} - x}.x

Free extension can introduce a duplicate.
let p = {x = 1} in {x = true | p}
let p = {x = 1} in ({x = true | p}).x
let p = {x = 1} in ({{x = true | p} - x}).x

Scoped labels inside nested records.
{outer = {x = 1, x = true}}
{outer = {x = 1, x = true}}.outer.x

Extension that shadows a polymorphic field type.
\r -> {x = 1 | r}
\r -> ({x = 1 | r}).x
}

The record {x = 1, x = true} infers as {x : Int, x : Bool} because both occurrences are preserved in the row. Selection {x = 1, x = true}.x picks the leftmost Int, while {x = true, x = 1}.x picks the leftmost Bool. Restriction peels one occurrence off at a time, so {{x = 1, x = true} - x}.x exposes the inner Bool. The same scoping rule applies to free extension: shadowing through \r -> {x = 1 | r} produces {r} -> {x : Int | r}, which when applied to an argument that already has an x yields a record with two x fields rather than a type error.

Selection

Selection is the operation that gives row polymorphism its name. Inside a lambda, selecting a field forces the row to be a variable, which generalises into the principal scheme \(\forall r, \alpha .\, \{l : \alpha \mid r\} \to \alpha\).

#![allow(unused)]
fn main() {
Selection in all its forms. Selection's principal type is
  (.l) : forall r a. {l : a | r} -> a

Direct selection from a literal.
{x = 42}.x

Selection through let.
let p = {x = 1, y = 2} in p.x
let p = {x = 1, y = 2} in {a = p.x, b = p.y}

Selection inside a lambda forces a row-polymorphic type.
\r -> r.x
\r -> r.foo

Two selections from the same row reuse the row variable.
\r -> \s -> r.x

Two selections from different records are independent.
\r -> \s -> r.x

Polymorphic selector functions.
let getx = \r -> r.x in getx {x = 1}
let getx = \r -> r.x in getx {x = true}
let getx = \r -> r.x in {a = getx {x = 1, y = 2}, b = getx {x = false, z = 3}}

Selection on extension.
({x = 1 | {y = 2}}).x
({x = 1 | {y = 2}}).y

Function returning a selector.
\l -> l.field

Higher-order: pass selector as argument.
\f -> \r -> f r

Compose selectors via let.
let getx = \r -> r.x in let gety = \r -> r.y in \r -> getx r
}

Direct selection from a literal like {x = 42}.x is trivial: the row exposes x at the head and the unifier accepts immediately. The interesting case is \r -> r.x, which has type {x : a | r} -> a. Inference introduces a fresh field type and a fresh tail, unifies the parameter’s row variable with the open shape, and generalisation closes over both new variables. Let-bound selectors like let getx = \r -> r.x in ... get the same scheme and can be applied at different record shapes, including ones with extra fields that the selector never inspects.

Extension

Free extension {l = e | r} prepends a field to a record without checking whether l already exists. This is what makes the principal scheme of extension \(\forall r, \alpha.\, \alpha \to \{r\} \to \{l : \alpha \mid r\}\) sound under scoped labels.

#![allow(unused)]
fn main() {
Free extension: {l = e | r}. Always succeeds; never overwrites.
Extension's principal type is
  {l = _ | _} : forall r a. a -> {r} -> {l : a | r}

Extension over the empty record.
{x = 1 | {}}
{x = 1, y = 2 | {}}

Extension over a literal.
{z = 0 | {x = 1, y = 2}}

Polymorphic extension.
\r -> {z = 0 | r}
\r -> {a = 1, b = 2, c = 3 | r}

Iterated extension (literal sugar already does this).
{a = 1 | {b = 2 | {c = 3 | {}}}}

Extension preserves the row variable for further use.
\r -> let s = {x = 1 | r} in s.x

Extension that introduces a duplicate label is fine.
\r -> {x = true | {x = 1 | r}}

Extension applied via let, used at multiple types.
let push = \r -> {z = 0 | r} in push {x = 1}
let push = \r -> {z = 0 | r} in push {y = true, w = false}

A function that builds a closed record from two arguments.
\x -> \y -> {first = x, second = y}

Extension and selection compose.
\r -> ({tag = 1 | r}).tag
\r -> ({tag = true | r}).tag

Mixing extension with subsequent selection of original fields.
let make = \r -> {extra = 0 | r} in (make {x = 1}).x
}

Extension over the empty record reconstructs the original literal: {x = 1 | {}} is {x : Int}. Extension over a polymorphic argument is row-polymorphic in the rest, so \r -> {z = 0 | r} has type {r} -> {z : Int | r}. The two push examples show that the same row-polymorphic extension function works at completely different record shapes through let-generalisation, instantiating the row variable once at each call site. Extension that introduces a duplicate label is intentionally allowed: \r -> {x = true | {x = 1 | r}} has type {r} -> {x : Bool, x : Int | r}, with the two x fields preserved in scope order.

Restriction

Restriction {r - l} peels off the leftmost occurrence of l, with principal scheme \(\forall r, \alpha.\, \{l : \alpha \mid r\} \to \{r\}\).

#![allow(unused)]
fn main() {
Restriction: {r - l}. Removes the leftmost l.
Principal type: (- l) : forall r a. {l : a | r} -> {r}

Restrict from a closed record.
{{x = 1, y = 2} - x}
{{x = 1, y = 2} - y}

Restrict to empty.
{{x = 1} - x}

Restrict from a polymorphic record.
\r -> {{x = 1 | r} - x}
\r -> {r - x}

Restrict twice (must restrict different labels or rely on duplicates).
{{{x = 1, y = 2, z = 3} - x} - y}
{{{x = 1, y = 2, z = 3} - z} - x}

Restrict the leftmost duplicate, then select the next.
{{x = 1, x = true} - x}.x
{{{x = 1, x = true, x = false} - x} - x}.x

Restrict and then extend (the basis for update).
\r -> {x = true | {r - x}}

Restrict from a let-bound polymorphic record.
let drop_x = \r -> {r - x} in drop_x {x = 1, y = 2}
let drop_x = \r -> {r - x} in drop_x {x = true, y = false, z = 99}

Restriction commutes with selection on a different label.
\r -> ({r - x}).y
\r -> ({{x = 1 | r} - x}).y
}

Restriction from a closed record reduces it: {{x = 1, y = 2} - x} has type {y : Int}. Restriction from a polymorphic record threads the row variable through: \r -> {r - x} has type {x : a | r} -> {r}. The combination \r -> {x = true | {r - x}} is the basis for an update operation that can change a field’s type, with the scheme {x : a | r} -> {x : Bool | r}. Restriction on a duplicate label exposes the inner occurrence, so {{x = 1, x = true} - x}.x returns the Bool.

Update

Update is syntactic sugar for restrict-then-extend: {l := e | r} desugars to {l = e | {r - l}}. Because the desugaring goes through restriction it is allowed to change a field’s type.

#![allow(unused)]
fn main() {
Update: {l := e | r} desugars to {l = e | {r - l}}.
Because of that desugaring, update can change a field's type.

Update preserving the type.
let p = {x = 1, y = 2} in {x := 99 | p}

Update changing the type (heterogeneous update).
let p = {x = 1, y = 2} in {x := true | p}

Update on a polymorphic record.
\r -> {x := 0 | r}
\r -> {x := true | r}

Update twice on the same label.
let p = {x = 1} in {x := false | {x := true | p}}

Update preserves the rest of the row.
let p = {x = 1, y = 2, z = 3} in ({x := true | p}).y
let p = {x = 1, y = 2, z = 3} in ({x := true | p}).z

Update on a duplicate field hits the leftmost (the duplicate stays).
let p = {x = 1, x = true} in {x := false | p}
let p = {x = 1, x = true} in ({x := false | p}).x

Updating creates a record whose row is open if the source is open.
\r -> ({x := 1 | r}).x

Building an updater function.
let setx = \v -> \r -> {x := v | r} in setx 42 {x = 1, y = 2}
let setx = \v -> \r -> {x := v | r} in setx true {x = 1}
}

Updating preserving the type, like {x := 99 | p} against {x = 1, y = 2}, gives back {x : Int, y : Int}. Heterogeneous update, like {x := true | p} against the same p, gives {x : Bool, y : Int} because the new field type replaces the old. A polymorphic updater \v -> \r -> {x := v | r} generalises to a scheme that lets the caller pick both the new value’s type and the rest of the row.

Polymorphism

Let-generalisation closes over both type and row variables. A function that uses a record polymorphically through let can be instantiated independently at each call site.

#![allow(unused)]
fn main() {
Let-polymorphism over both type and row variables.

A row-polymorphic function used at two different row instantiations.
let getx = \r -> r.x in {a = getx {x = 1}, b = getx {x = true}}

Identity is row-polymorphic when applied to records.
let id = \x -> x in id {x = 1, y = true}
let id = \x -> x in {a = id {x = 1}, b = id {y = false, z = 0}}

Polymorphism in both the field type and the row tail.
let getx = \r -> r.x in getx
let drop_x = \r -> {r - x} in drop_x

Records of polymorphic functions: each field gets its own scheme on use.
let p = {id = \x -> x, fst = \x -> \y -> x} in p

Records carrying functions used at multiple types.
let p = {id = \x -> x} in p

Generalization respects free variables in the environment.
\r -> let getx = \s -> s.x in getx r

Compose two row-polymorphic projections.
let getx = \r -> r.x in let gety = \r -> r.y in \r -> getx {dummy = gety r | r}

Function whose type is forall r a. {x : a | r} -> a.
\r -> r.x

Two independent row variables in a single signature.
\r -> \s -> {a = r.x, b = s.y}

Higher-rank-flavored use: a record selector returned from let.
let mk = \k -> \r -> r in mk 0 {x = 1}
}

The first example, let getx = \r -> r.x in {a = getx {x = 1}, b = getx {x = true}}, exercises both row and field polymorphism: the same selector is applied at {x = 1} and {x = true}, and the result is {a : Int, b : Bool}. Records carrying polymorphic values like {id = \x -> x, fst = \x -> \y -> x} infer principal field types {id : a -> a, fst : b -> c -> b}, with each field’s scheme independent. The last entry is the canonical row-polymorphic selector with two independent rows, \r -> \s -> {a = r.x, b = s.y}, which has type {x : a | r} -> {y : b | s} -> {a : a, b : b}.

Termination

The side condition in row unification is what rules out the divergent cases identified by Wand. These examples are deliberately the kind of programs that without the side condition would force the algorithm to bind the same tail variable twice.

#![allow(unused)]
fn main() {
Termination corner cases for row unification.
The side condition `tail(r) ∉ dom(θ1)` in (uni-row) prevents these from
diverging (Leijen 2005, sect. 7.1).

The classic non-terminating example from Wand. Both branches share the row
variable r. Without the side condition, unifying {x : Int | r} ~ {y : Int | r}
would loop. With it, inference completes and the function is row-polymorphic
in r but contributes both labels to the result.
\r -> let f = \c -> {x = 1 | r} in let g = \c -> {y = 2 | r} in f

Same idea, three different labels.
\r -> let f = \c -> {x = 1 | r} in let g = \c -> {y = 2 | r} in let h = \c -> {z = 3 | r} in f

Common-tail unification with field types that must agree.
\r -> let mk = \c -> {x = c | r} in mk

Two records over the same tail, used independently.
\r -> let a = {x = 1 | r} in let b = {y = true | r} in a

Adding fields one-by-one.
\r -> {a = 1 | {b = 2 | {c = 3 | r}}}

Open record in, open record out, types fully inferred.
\r -> {x := r.x | r}

Selection from a row variable (infers a row-polymorphic record).
\r -> r.field

Round-trip: restrict then extend with a fresh value of the same label.
\r -> {x = 0 | {r - x}}

Two rows of unknown shape, unified by selection.
\r -> \s -> let pair = {a = r.x, b = s.x} in pair

A function whose argument record must contain at least three labels.
\r -> {p = r.x, q = r.y, s = r.z}
}

The first example builds two extension functions that share a row variable r but extend with different labels, then selects only one. Inference must not commit r to be both {x : Int | _} and {y : Int | _} at the same time. Because only f is returned, the side condition lets the program type-check with f’s scheme {r} -> a -> {x : Int | r}, deferring the conflict that never materialises. The genuine conflict shows up in the errors file, where forcing the unification produces RecursiveRow.

Errors

Failed inferences produce typed error messages rather than panics. The errors file is the negative half of the test suite: each line is expected to fail.

#![allow(unused)]
fn main() {
Type errors. Each line should produce an error rather than a type.

Selection of a label not present in a closed record.
{x = 1}.y
{x = 1, y = 2}.z

Selection from the empty record.
{}.x

Restriction of a label not present.
{{x = 1} - y}
{{} - x}

Use a row-polymorphic projection at two incompatible field types.
let getx = \r -> r.x in let f = getx {x = 1} in getx {x = true}

Force unification of two row tails carrying conflicting field types for x.
\r -> \k -> let a = {x = 1 | r} in let b = {x = true | r} in k a b

Genuine Wand-style trigger for the (uni-row) side condition: the same `k`
is applied to two records that share row tail `r` but disagree on the head
label, forcing {x : Int | r} ~ {y : Int | r}. The side condition catches
this as a recursive row binding rather than diverging.
\r -> \k -> let dummy = k {x = 1 | r} in k {y = 2 | r}

Selection on a non-record (an Int).
(\x -> x.foo) 1

Applying a record where a function is expected.
{x = 1} 2

Extending a non-record.
{l = 1 | 42}

Occurs check on type variables (classic self-application).
\x -> x x

Mismatched arrow vs record.
(\f -> f 1) {x = 1}

Unifying two closed records of different shapes (no tuple support; use sequencing).
let f = \r -> r.x in let p = {x = 1} in let q = {y = 2} in f q
}

Selection of a missing label, like {x = 1}.y, reports Label 'y' missing from row {}. Restriction of a missing label reports the same. The Wand-style trigger, \r -> \k -> let dummy = k {x = 1 | r} in k {y = 2 | r}, forces {x : Int | r} ~ {y : Int | r} and is caught by the side condition as Recursive row unification: tail variable 'r5' would be bound twice. Selection on a non-record like (\x -> x.foo) 1 fails with a structural mismatch between {foo : t2 | r3} and Int, and applying a record where a function is expected fails the same way in the opposite direction.