Record types

In the type declarations discussed above, the arguments to each data constructor are nameless. For example:

structural type Point = Point Nat Nat

Here, the data type has one constructor, with two arguments, both of type Nat. The arguments have no name, so they are identified positionally, for example when creating a value of this type, like Point 1 2.

Types with a single data constructor can also be defined in the following style, in which case they are called record types.

Point2 = {x : Nat, y : Nat}

This assigns names to each argument of the constructor. The effect of this is to generate some accessor methods, to help get, set, and modify each field.

• Point2.x : Point2 -> Nat
• x.modify : (Nat ->{g} Nat) -> Point2 ->{g} Point2
• x.set : Nat -> Point2 -> Point2
• y : Point2 -> Nat
• y.modify : (Nat ->{g} Nat) -> Point2 ->{g} Point2
• y.set : Nat -> Point2 -> Point2

There's currently no special syntax for creating, pattern matching, or decomposing records. That works the same as for regular data types:

p = Point2 1 2
let
  (Point2 x _) = p
  x
⧨
1