Skip to main content

Row polymorphism

TL;DR. The type { x: Int | r } — "a record with at least x: Int, where r stands for the rest" — is part of the grammar and parses today. It does not yet constrain anything: a record without x is accepted where one is required. The expression-level half of the design (anonymous record literals, the pipe-splat, lacks predicates) is not implemented at all.

Status — measured, not planned

Every row in the table at the end of this page was measured with verum check on 2026-09-03, each probe differing from its control in one value. Three things this page previously called Stable do not work. Read the table before building on the feature.

The idea​

A closed record type { x: Int, y: Int } names exactly two fields. An open one, { x: Int | r }, is meant to say "at least x: Int; r captures whatever else is there", so one function serves every record that carries the fields it actually reads:

fn get_x<r>(p: { x: Int | r }) -> Int { p.x }

That is the design. What follows is where the implementation stands.

What parses and works​

Open record types in a signature. grammar/verum.ebnf:1403 gives

record_type = '{' , [ field_list ] , [ '|' , identifier ] , '}' ;

so { x: Float, y: Float | r } is grammatical in any type position, and the parser builds it (TypeKind::Record { fields, row_var }). A function declared that way compiles, and a Point passed to it is accepted.

Note the grammar admits one row variable, not a list: { x: Int | r, s } is not the language.

Record update, with the comma spelling. A functional update exists — field_inits ends with an optional '..' , expression:

type P is { a: Int, b: Int };

let base = P { a: 1, b: 2 };
let plus = P { a: 5, ..base };     // ok: b comes from base

It requires the named type in front and a comma before ...

What does not work yet​

The open record type constrains nothing. Both of these are accepted:

type Point is { x: Float, y: Float };
type Only  is { z: Float };

fn dist<r>(p: { x: Float, y: Float | r }) -> Float { p.x }

dist(Point { x: 3.0, y: 4.0 });   // accepted — correct
dist(Only { z: 1.0 });            // ALSO accepted — should be refused

The second call passes a record that has neither x nor y. The row type is currently syntax without a check, so it documents intent rather than enforcing it.

Anonymous record literals do not exist. record_expr = path , '{' , field_inits , '}' requires a named type, so

let base = { a: 1, b: 2 };        // error<E100>: unbound variable: a

the braces are parsed as a block, and a as an expression.

The pipe-splat is not the update syntax — and it silently means something else. This page used to show { c: 3 | ..base }. With a named type in front it parses, but as a bitwise or of 3 with the range ..base:

let plus = P { a: 5 | ..base };
// error<E400>: Type mismatch in field 'a' of 'P':
//              expected 'Range<P>', found 'Int'

Use the comma spelling above.

Lacks predicates are a parse error. where r # y — the constraint this page described as threaded through inference — is not in the grammar and not in the parser:

fn rename<r>(p: { x: Int | r }) -> Int where r # y { p.x }
// error<E032>: Parse error: expected `{` to start function body

Consequently the error message this page quoted (row `r` must lack field `x` ) is not one the compiler can produce.

Status​

FeatureStatusMeasured
Open record type parses ({ x: T | r })Worksin a signature, accepted
Open record type checksNot implementeda record lacking the named fields is accepted
Record update P { a: 5, ..base }Works0 errors
Anonymous record literal { a: 1 }Not implementedE100 — parsed as a block
Pipe-splat { a: 5 | ..base }Not implementedparses as bit-or with a range
Lacks predicate where r # yNot implementedE032 parse error
Two row variables { x: T | r, s }Not in the grammarone row variable only
Row-based protocol dispatchPlanned—

See also​