Records

See the official user manual for the most up-to-date version of the information on this page.

TOC

There is a fine tutorial on records for a more detailed tour.

Records are types for grouping values together. They generalise the dependent product type by providing named fields and (optional) further components.

The general form of a record declaration is as follows:

  record <name> <parameters> : Set <level> where
    constructor <operator>
    field
       <fname> : <ty>
       <fname> : <ty>
       ...
    <declaration>
    ...

This defines a record type.

All the components are optional, and can be given in any order. In particular, fields can be given in more than one block, interspersed with other declarations.

Every record declaration introduces a module with the same name. For more about this module, see the Modules section.

The constructor, if included, will be defined as a function from field values to a record value.

Each field is a component of the record. Types of later fields can depend on earlier fields.

Further declarations, which may depend on fields above them, become components of values of the record type that are computed from the fields.

Record values are created as follows.

  <constructor> <tm> <tm> ...

or

  record { <fname> = <tm> ; <fname> = <tm> ; ... }

Given a value r of a record type, its fields (and other components), can be accessed as follows.

  <name>.<fname> <r>

But by applying the module associated with the record type to a record value, and opening the resulting module, the value's components can be brought directly into scope.

Record pattern matching

It is now possible to pattern match on named record constructors. Example:

  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B proj₁

  map : {A B : Set} {P : A → Set} {Q : B → Set}
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
  map f g (x , y) = (f x , g y)

The clause above is internally translated into the following one:

  map f g p = (f (Σ.proj₁ p) , g (Σ.proj₂ p))

Record patterns containing data type patterns are not translated. Example:

  add : ℕ × ℕ → ℕ
  add (zero  , n) = n
  add (suc m , n) = suc (add (m , n))

Record patterns which do not contain data type patterns, but which do contain dot patterns, are currently rejected. Example:

  Foo : {A : Set} (p₁ p₂ : A × A) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
  Foo (x , y) (.x , y′) refl = Set