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: