Record types

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

structural type Point1

structural type Point1 = Point2 Nat Nat

Here, the data typePoint1has a constructorPoint2,with two arguments, both of typeNat.The arguments have no name, so they are identified positionally, for example when creating a value of this type, likePoint2 1 2.

Types with a single data constructor can also be defined in the following style, in which case they are calledrecord 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