Records Tutorial

This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0. It uses the standard library, the following imports should be used to check this file:

```  open import Data.Bool
open import Data.Nat
open import Data.Vec hiding (map)
open import Data.Product
```

Basics

How to declare record types

Record types make it possible to put values together. Their values are tuples of values of specified types. For instance, the type `R` in the following code snippet introduces a record type of pairs of values of type `Bool` and those of type `ℕ`.

```  b : Bool    -- example value of type Bool
b = false

n : ℕ
n = 2       -- example value of type ℕ

record R : Set where
field
f1 : Bool
f2 : ℕ
```

`f1` and `f2` are the ‘field names’ of the record type `R`.

How to construct values of record types

What are the values of type `R`? Given a term `b` of type `Bool` and `n` of type `ℕ`, `record { f1 = b; f2 = n }` is a term of type `R`, and all values of `R` are obtained in this way, in the sense that every term of type `R` is convertible to a term of this form.

So, we may have a declaration like

```  r : R
r = record { f1 = b
; f2 = n
}
```

Note that the semicolon (;) is necessary here.

How to decompose values of record types

With the field name, we can select the corresponding component out of a value of type `R`. In fact, we may think the two functions with the following types are attached to the above declaration of type `R`.

```  R.f1 : R -> Bool
R.f2 : R -> ℕ
```

Example

Suppose that we want to define a function that increases the second component of an `R` record by one. We can write:

```  increaseInR : R -> R
increaseInR r = record { f1 = R.f1 r ; f2 = suc (R.f2 r) }
```

Explicit record constructors

In Agda 2.2.6 the support for explicit record constructors was added.

We can write an improved version of the `R` record type:

```  record R2 : Set where
constructor r2             -- new!
field
f1 : Bool
f2 : ℕ
```

Notice that the `constructor` and `field` keywords have to be indented by the same number of spaces.

Values of `R2` can now be created in two ways:

```  -- the same as before
rA : R2
rA = record { f1 = b
; f2 = n
}

-- using the r2 constructor
rB : R2
rB = r2 b n
```

It’s possible to trivially prove that `rA` and `rB` are convertible:

```  -- the propositional equality relation

data _≡_ {A : Set} : (a b : A) -> Set where
refl : {a : A} → a ≡ a

recordsEqual : rA ≡ rB
recordsEqual = refl
```

Details

From Agda 2.2.6 release notes:

Record constructors can be defined:

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

In this example _,_ gets the type

```  (proj₁ : A) → B proj₁ → Σ A B.
```

For implicit fields the corresponding constructor arguments become implicit.

Note that the constructor is defined in the outer scope, so any fixity declaration has to be given outside the record definition. The constructor is not in scope inside the record module.

Pattern matching on records

In the increaseInR example mentioned earlier, it might seem natural to pattern match on `r` but it’s not allowed. However, pattern matching is possible when the record type has been declared with a constructor - see below:

```  increaseInR2 : R2 -> R2
increaseInR2 (r2 f1 f2) = r2 f1 (suc f2)
```

Details

From Agda 2.2.8 release notes:

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

NOTE: In Agda 2.2.8 and 2.2.10 record patterns which did not contain data type patterns, but which contained dot patterns, were rejected. This has been changed in Agda 2.3.0. The following example works now:

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

Conversion rules for record types

Record field projections described above are subject to the following equations. For any term `r : R`:

``` R.f1 r ≈ b
R.f2 r ≈ n
r      ≈ record { f1 = R.f1 r
; f2 = R.f2 r
}
```

Since `R2` has a constructor r2 defined, we also have, for any term `r’ : R2`

``` r’ ≈ r2 (R2.f1 r’) (R2.f2 r’)
```

Example.

```  record Pair : Set where
constructor pair
field
fst : ℕ
snd : ℕ

extRec : (r : Pair) → r ≡ pair (Pair.fst r) (Pair.snd r)
extRec _ = refl
```

To prove extRec we don’t even need to pattern match on r - Agda converts `pairR (PairR.fst r) (PairR.snd r)` to `r` automatically (this can be seen using the interactive emacs mode).

Difference with ‘data’ declarations

We can define a type with exactly one value both as a record and using the ‘data’ keyword.

```  record TrueR : Set where
constructor ttR

data TrueD : Set where
ttD : TrueD
```

Now let’s try to prove the ‘exactly one value’ lemmas:

```  alwaysTrueR : (t : TrueR) -> t ≡ ttR
alwaysTrueR _ = refl

alwaysTrueD : (t : TrueD) -> t ≡ ttD
alwaysTrueD ttD = refl
```

In the former case we don’t have to pattern match, but the latter case won’t work without pattern matching.

From a practical standpoint, it means that you can assert to Agda that your function that returns a certain type (say a pair) always produces an inhabited value. On the other hand, single-constructor data types may not be inhabited if their indices can’t be satisfied (take refl and the equality type, for example).

Recursive records

Record types whose fields refer to the type being defined must be declared either `inductive` or `coinductive` by placing the relevant keyword in the record definition, aligned to match the `constructor` and `field` keywords. Failure to do so will produce an error:

```  Recursive record Foo needs to be declared as either inductive or coinductive
```

‘Dependent’ records

Agda has dependent types. The type of a field of record type can depend on the values of the fields of the same record type that appear previously in the declaration of the record type. For instance, a type `VecB` of lists of Booleans, parameterised by their length may be declared as follows.

```  infixr 5 _∷_
data Vec (X : Set) : ℕ -> Set where
[]   : Vec X zero
_∷_ : {n : ℕ} -> X -> Vec X n -> Vec X (succ n)

VecB : ℕ -> Set
VecB = Vec Bool

v : VecB n
v = false ∷ (true ∷ []) -- example value of VecB n
```

VecB takes a parameter of type `ℕ` and returns a type. Then, the type `VR` of pairs of a natural number `n` and a value of `VecB n` can be declared in the following way.

```  record VR : Set where
field
length : ℕ
vector : VecB length
```

The followings are examples of value of `VR`:

```  vr1 : VR
vr1 = record { length = zero ; vector = [] }

vr2 : VR
vr2 = record { length = suc zero ; vector = true ∷ [] }

vr : VR
vr = record { length = n ; vector = v }
```

… and nonexamples:

``` record { length = succ zero ; vector = [] }
-- the type of vector field is VecB(zero), not VecB(succ zero), i.e., VecB(length)
record { length = succ zero ; vector = false ∷ (true ∷ []) }
-- the type of vector field is VecB(succ (succ zero)), not VecB(succ zero), i.e., VecB(length)
```

Here, the type of the field `vector` depends on the values of the previous fields, as its type contains the name of the first field `length`.

Selectors for dependent records are a bit tricky, as one needs provide the parameter to the field name, to obtain the proper target type. The above record type declaration brings the following two functions:

``` VR.length : VR -> ℕ
VR.vector : (vr : VR) -> VecB (VR.length vr)
```

In the same way as nondependent case, we have the following convertibility.

```  VR.length vr ≈ n
VR.vector vr ≈ v
v            ≈ record { length = VR.length vr
; vector = VR.vector vr
}
```

Parameterised Record Types

Record types may have parameters. For instance, we may declare a type taking a type parameter `X` and returning a record type for pairs of natural numbers and vectors of that length, whose elements are taken from `X`, in the following way.

```  record VRP (X : Set) : Set where
field
len : ℕ
vec : Vec X len

vrpNat : VRP ℕ
vrpNat = record { len = suc (suc zero)
; vec = zero ∷ (suc zero ∷ [])
}
```

Implicit fields

Since Agda 2.2.6 record fields can be implicit:

```  record RI : Set₁ where         -- Contains fields from Set so can’t be in Set itself
field
{B}         : Set
f           : B -> B
{D F} E {G} : Set
g           : D -> F -> G
```

By default implicit fields are not printed.

Irrelevant fields

You can learn about irrelevance in the Irrelevance chapter.

Since Agda 2.2.8 record fields can be made irrelevant. Example:

```  record Subset (A : Set) (P : A → Set) : Set where
constructor _#_
field
elem   : A
.proof : P elem
```

Irrelevant fields are never in scope, neither inside nor outside the record. This means that no record field can depend on an irrelevant field.

In Agda 2.2.8 projections were not defined for irrelevant fields, they could have only been accessed using pattern matching.

Since Agda 2.2.10 projections are generated automatically for irrelevant fields (unless the flag —no-irrelevant-projections is used). However, note that irrelevant projections are highly experimental.

Records with only irrelevant fields

Since Agda 2.3.0 the following works:

```  record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where
field
.refl  : Reflexive _≈_
.sym   : Symmetric _≈_
.trans : Transitive _≈_

record Setoid : Set₁ where
infix 4 _≈_
field
Carrier        : Set
_≈_            : Carrier → Carrier → Set
.isEquivalence : IsEquivalence _≈_

open IsEquivalence isEquivalence public
```

Previously Agda complained about the application IsEquivalence isEquivalence, because isEquivalence is irrelevant and the IsEquivalence module expected a relevant argument. Now, when record modules are generated for records consisting solely of irrelevant arguments, the record parameter is made irrelevant:

```  module IsEquivalence {A : Set} {_≈_ : A → A → Set}
.(r : IsEquivalence {A = A} _≈_) where
…
```

General Syntax and Meaning

A record type in general is declared in the following way.

``` record R Δ : Set where
field
x1 : A1[y1, …, ym-1]
x2 : A2[y1, …, ym-1, x1]
…
xn : An[y1, …, ym-1, x1…xn-1]
```

Here, Δ represents a ‘telescope’, which is of the following form

``` (y1 : B1) (y2 : B2[y1]) … (ym : Bm[y1…ym-1])
```

Note that `B2[y1]`, for instance, does not mean `B2` is applied to `y1`, but it means the term `B2` may have free occurrences of the variable `y1`, but of no other variables. With that understanding, one could have simply written `B2`. Likewise, `An[x1…xn-1]` in the record declaration only denotes the term `An`, and if it has a free occurences of any variable, that is amongst `x1``xn-1`.

This declaration introduces the following identifiers to the system:

``` R : (y1 : B1) -> … -> (ym : Bm) -> Set
R.x1 : {y1 : B1} -> … -> {ym : Bm} -> R y1 … ym -> A1
R.x2 : {y1 : B1} -> … -> {ym : Bm} -> (r : R y1 … ym) -> A2[y1, …, ym, R.x1 r]
…
R.xn : {y1 : B1} -> … -> {ym : Bm} -> (r : R y1 … ym) -> An[y1, …, ym, R.x1 r, … , R.xn r]
```

`R` itself is the parameterised record type, and `R.x1`, …, `R.xn` are projectors of `R`. Note that paremeters `y1`, …, `ym` given to the projectors are made implicit here, since their values could be inferred from the type of `r` in many cases.

Opening a record to bring the fields into scope

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[y1, …, ym-1]
x1 = …
x2 : A2[y1, …, ym-1, x1]
x2 = …
…
xn : An[y1, …, ym-1, 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 R r
```

Record opening example

Suppose we have:

```  record Example : Set where
field
bool : Bool
nat  : ℕ

ex : Example
ex = record { bool = true ; nat = 3 }
```

We want to extract the fields of `ex`, but writing (for example) `Example.bool ex` may get tiring after a short while. What can we do about it?

Without opening the Example the module we don’t have any choice:

```  -- this won’t work here - nat is not in scope

-- correct way - fully qualified projection
correct : ℕ
correct = Example.nat ex
```

However, we can open the Example module generated for the Example record and get shorter projection functions. If we don’t want to pollute the whole top-level module with the new names we can open it inside a module or for a single declaration (see below).

```  module Open1 where
open Example

-- here we have:
-- bool : (r’ : Example) → Bool
-- nat  : (r’ : Example) → ℕ

test : ℕ
test = nat ex

test2 : ℕ
test2 = nat ex where open Example
```

We can also open the Example module for a given record value, thus bringing all of its fields into the scope at once:

```  module Open2 where
open Example ex

-- here we have:
-- bool ≡ true : Bool
-- nat  ≡ 3    : ℕ

test : ℕ
test = nat

test2′ : ℕ
test2′ = nat where open Example ex
```

Record update syntax

Assume that we have a record type and a corresponding value:

```  record MyRecord : Set where
field
x y z : ℕ

old : MyRecord
old = record { x = 1; y = 2; z = 3 }
```

Then we can update (some of) the record value’s fields in the following way:

```  new : MyRecord
new = record old { x = 0; z = 5 }
```

Here `new` normalises to `record { x = 0; y = 2; z = 5 }`. Any expression yielding a value of type `MyRecord` can be used instead of `old`.

Record updating is not allowed to change types: the resulting value must have the same type as the original one, including the record parameters. Thus, the type of a record update can be inferred if the type of the original record can be inferred.

The record update syntax is expanded before type checking. When the expression

```  record old { upd-fields }
```

is checked against a record type R, it is expanded to

```  let r = old in record { new-fields },
```

where old is required to have type R and new-fields is defined as follows: for each field x in R,

```  - if x = e is contained in upd-fields then x = e is included in
new-fields, and otherwise
- if x is an explicit field then x = R.x r is included in
new-fields, and
- if x is an implicit or instance field, then it is omitted from
new-fields.
```

(Instance arguments are explained here.) The reason for treating implicit and instance fields specially is to allow code like the following:

```  record R3 : Set where
field
{length} : ℕ
vec      : Vec ℕ length
-- More fields…

xs : R3
xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }

ys = record xs { vec = 0 ∷ [] }
```

Without the special treatment the last expression would need to include a new binding for length (for instance “length = _”).

Extending the record module with additional functions

```  record A : Set where
constructor constr
field
n1 : ℕ
n2 : ℕ

swapA : A
swapA = record { n1 = n2 ; n2 = n1 }

-- the A record type in action
a : A
a = constr 0 1

a2 : A
a2 = A.swapA a       -- swap is generalized outside the
-- “definition scope” and here has type (r’ : A) → A !
```

Notice that when we define the swap “virtual selector” we can’t access the constructor `constr` on both the left and right hand side.

More examples

Private definitions:

```  record WithPriv (A : Set) : Set where
private
l : Vec ℕ (suc (suc zero))
l = zero ∷ (suc zero ∷ [])
field
first : A
```

Extracting an implicit field:

```  record Implicit : Set where
constructor impl
field
{k} : ℕ
vec : Vec ℕ k

get : Implicit -> ℕ
get = Implicit.k

get2 : Implicit -> ℕ
get2 (impl {k} vec) = k
```

References

History of changes of the support for records in Agda:

• implicit arguments and constructors for records.
• pattern matching on records, irrelevant fields
• projections generated automatically for irrelevant fields