Records

A record is a special data type which contain one or more data constructors, each with labeled type arguments.

For example, the following defines a record type Person with a single constructor mkPerson that takes two arguments, name and age, of types String and Nat, respectively.

  type Person :=
    mkPerson {
      name : String;
      age : Nat
    };

In each type constructor of the record, the type arguments are called fields. Each field consists of a name and type. The field's name can be used to access to the value connected with the term of the record type.

The syntax for declaring a record type is as follows:

type <record name> <type parameters> :=
    | <type-constructor1> {
        <field1-1> : <type1-n>;
        ...
        <field1-n> : <type1-n>
        }
    | ...
    | <type-constructor-n> {
        <fieldn-1> : <typen-1>;
        ...
        <fieldn-n> : <typen-n>
    };

Using Records

Records are just like any other data type. They can be used in local definitions, exported from a module, and used in pattern matching.

That is, one could define a record with a single constructor or multiple constructors. For instance, here is an example declaring the newType record type declaration with the mkNewtype type constructor and one filed named f.

type T := constructT : T;

type newtype := mkNewtype {f : T};

We could also define a record with multiple constructors. For instance, let us define the record type called Pair to model pairs of values. The Pair type has a single mkPair type constructor that takes two arguments, called fst and snd, of types A and B, respectively.

type Pair (A B : Type) :=
  mkPair {
    fst : A;
    snd : B
  };

To use this type, create a Pair type term (a pair) using the mkPair type constructor and supplying values for each field.

p1 : Pair T T :=
  mkPair (fst := constructT; snd := constructT);

Field names enable access to their associated values. For instance, another pair equivalent to the one defined above can be declared using values extracted via the field names.

p1' : Pair T T :=
  mkPair (fst := Pair.fst p1; snd := Pair.snd p1);

The fields record type's fields are qualified by the type name by default. To access the fields without the type name, use the open keyword to bring these names into scope.

open Pair;

flipP : Pair T T := mkPair (fst := snd p1; snd := fst p1);

Lastly, let us declare a record with multiple constructors.

type EnumRecord :=
  | C1 {
      c1a : T;
      c1b : T
    }
  | C2 {
      c2a : T;
      c2b : T
    };

p2 : Pair EnumRecord EnumRecord :=
  mkPair
    (fst := C1 (c1a := constructT; c1b := constructT);
    snd := C2 (c2a := constructT; c2b := constructT));

Comments