← Docs

Records

A record declaration introduces a type together with projection per field, and the type satisfies a definitional eta rule so two records should be equal exactly when their fields are.

Declaration

A record is declared with \record, followed by the type and one | field : T line per field.

\record Point : 𝓤
  | x : Nat
  | y : Nat

Each field becomes a qualified projection: the declaration above gives you Point/x : Point -> Nat and Point/y : Point -> Nat, the same convention used for inductive constructors.

Construction

Build a record by giving every field a value. Order of fields in the literal does not matter — they are matched by name.

\let origin : Point => { x => Nat/zero | y => Nat/zero }

Punning

When a variable already in scope shares a field name, you can drop the => value part. { x | y } desugars to { x => x | y => y }.

\let pt (x : Nat) (y : Nat) : Point => { x | y }

Function fields

When a field's type is a function, you can name its parameters to the left of => instead of writing an explicit lambda — field p1 … pn => body desugars to field => \p1 … pn -> body. The parameters' type (and any implicits) are recovered from the field's declared type.

\record Endo : 𝓤
  | run : Nat -> Nat

# these two are the same record
\let inc : Endo => { run n => Nat/suc n }
\let inc' : Endo => { run => \n -> Nat/suc n }

Field projection

Read fields by applying the qualified projection — the same pattern as Nat/suc on an inductive type.

\let origin-y : Nat => Point/y origin

Or we can use dot syntax

\let origin-y : Nat => origin.y

Update

Records are immutable, but you can build a new record from an existing one by overriding some fields. The syntax mirrors a record literal with a base before the \with keyword:

\let update-x : Point => { origin \with x => Nat/suc Nat/zero }

Fields that are not mentioned are copied from the base. List multiple overrides separated by |, and punning works just like in a plain literal — { origin \with x } means { origin \with x => x }:

\let update-both : Point =>
  { origin \with x => Nat/suc Nat/zero | y => Nat/suc (Nat/suc Nat/zero) }

\let bump-x (x : Nat) : Point => { origin \with x }

At least one field is required — { origin \with } is rejected — and every name after \with must already be a field of the record's type.