Record Types

Note

This is a stub.

Record declarations

Record types can be declared using the record keyword

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

This defines a new type Pair : Set → Set → Set and two projection functions

Pair.fst : {A B : Set} → Pair A B → A
Pair.snd : {A B : Set} → Pair A B → B

Elements of record types can be defined using a record expression

p23 : Pair Nat Nat
p23 = record { fst = 2; snd = 3 }

or using Copatterns

p34 : Pair Nat Nat
Pair.fst p34 = 3
Pair.snd p34 = 4

Record types behaves much like single constructor datatypes (but see eta-expansion below), and you can name the constructor using the constructor keyword

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

p45 : Pair Nat Nat
p45 = 4 , 5

Note

Naming the constructor is not required to enable pattern matching against record values. Record expression can appear as patterns.

Record modules

Along with a new type, a record declaration also defines a module containing the projection functions. This allows records to be “opened”, bringing the fields into scope. For instance

swap : {A B : Set} → Pair A B → Pair B A
swap p = snd , fst
  where open Pair p

It possible to add arbitrary definitions to the record module, by defining them inside the record declaration

record Functor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ fb = fmap (λ _ → x) fb

Note

In general new definitions need to appear after the field declarations, but simple non-recursive function definitions without pattern matching can be interleaved with the fields. The reason for this restriction is that the type of the record constructor needs to be expressible using let-expressions. In the example below D₁ can only contain declarations for which the generated type of mkR is well-formed.

record R Γ : Setᵢ where
  constructor mkR
  field f₁ : A₁
  D₁
  field f₂ : A₂

mkR : ∀ {Γ} (f₁ : A₁) (let D₁) (f₂ : A₂) → R Γ

Eta-expansion

Instance fields

Instance fields, that is record fields marked with {{ }} can be used to model “superclass” dependencies. For example:

record Eq (A : Set) : Set where
  field
    _==_ : A → A → Bool

open Eq {{...}}

record Ord (A : Set) : Set where
  field
    _<_ : A → A → Bool
    {{eqA}} : Eq A

open Ord {{...}} hiding (eqA)

Now anytime you have a function taking an Ord A argument the Eq A instance is also available by virtue of η-expansion. So this works as you would expect:

_≤_ : {A : Set} {{OrdA : Ord A}} → A → A → Bool
x ≤ y = (x == y) || (x < y)

There is a problem however if you have multiple record arguments with conflicting instance fields. For instance, suppose we also have a Num record with an Eq field

record Num (A : Set) : Set where
  field
    fromNat : Nat → A
    {{eqA}} : Eq A

open Num {{...}} hiding (eqA)

_≤3 : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → A → Bool
x ≤3 = (x == fromNat 3) || (x < fromNat 3)

Here the Eq A argument to _==_ is not resolved since there are two conflicting candidates: Ord.eqA OrdA and Num.eqA NumA. To solve this problem you can declare instance fields as overlappable using the overlap keyword:

record Ord (A : Set) : Set where
  field
    _<_ : A → A → Bool
    overlap {{eqA}} : Eq A

open Ord {{...}} hiding (eqA)

record Num (A : Set) : Set where
  field
    fromNat : Nat → A
    overlap {{eqA}} : Eq A

open Num {{...}} hiding (eqA)

_≤3 : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → A → Bool
x ≤3 = (x == fromNat 3) || (x < fromNat 3)

Whenever there are multiple valid candidates for an instance goal, if all candidates are overlappable, the goal is solved by the left-most candidate. In the example above that means that the Eq A goal is solved by the instance from the Ord argument.

Clauses for instance fields can be omitted when defining values of record types. For instance we can define Nat instances for Eq, Ord and Num as follows, leaving out cases for the eqA fields:

instance
  EqNat : Eq Nat
  _==_ {{EqNat}} = Agda.Builtin.Nat._==_

  OrdNat : Ord Nat
  _<_ {{OrdNat}} = Agda.Builtin.Nat._<_

  NumNat : Num Nat
  fromNat {{NumNat}} n = n