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 Γ
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