Records

A record type is declared as follows:

 record R Δ : Set where
  field
   x1 : A1
   x2 : A2[x1]
   ...
   xn : A_n[x1... xn-1]

where x1...xn are the fields of the record. Note that the types of later fields can depend on the values of the previous fields.

Two things that one might want for a record type are suitably named projection functions and some way of opening a record to bring the fields into scope. It turns out that using the module system we can get both things for the price of one. For the record R above, we generate a parametrised module R

 module R {Δ}(r : R Δ) where
   x1 : A1
   x1 = ...
   x2 : A2[x1]
   x2 = ...
   ...
   xn : An[x1 ... xn-1]
   xn = ...

The functions in R are exactly the projection functions for the record type R. For instance, we have R.x2 : {Δ}(r : R Δ) -> A2[R.x1 r]. (So, what in some languages is written r.x2 for r : R, we write as R.x2 r.) Here it is clear that we want the parameters to the record to be implicit regardless of whether they are implicit arguments to the record or not. Now the nice thing is that we can apply the module to a given record, effectively projecting all fields from the record at once, which is exactly what we are looking for in a record open feature. So to open a record r : R we simply say

 open module M = R r

See examples/lattice for an example of how to use the module system and the record types together.