This document has been extracted from a literate agda file, which was tested with Agda 2.2.10

Table of contents

  1. Basics
    1. How to declare record types
    2. How to construct values of record types
    3. How to decompose values of record types
    4. Example
  2. Explicit record constructors
    1. Details
  3. Pattern matching on records
    1. Details
  4. Conversion rules for record types
  5. 'Dependent' records
  6. Parameterised Record Types
  7. Implicit fields
  8. Irrelevant fields
  9. General Syntax and Meaning
    1. Opening a record to bring the fields into scope
  10. Extending the record module with additional functions
  11. More examples
  12. References
    1. History of changes of the support for records in Agda:

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 Nat.

  data Bool : Set where
    true  : Bool
    false : Bool

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

  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

  n : Nat
  n = succ (succ zero) -- example value of type Nat

  record R : Set where
    field
      f1 : Bool
      f2 : Nat

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 Nat, 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 -> Nat

Example

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

  increaseInR : R -> R
  increaseInR r = record { f1 = R.f1 r ; f2 = succ (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 : Nat

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 (succ 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 : Nat → Nat → Nat
  add zero     n = n
  add (succ m) n = succ (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

Conversion rules for record types

Moreover, these 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')

'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, which appears 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.

  data Vec (X : Set) : Nat -> Set where
     []   : Vec X zero
     _::_ : {n : Nat} -> X -> Vec X n -> Vec X (succ n)

  VecB : Nat -> Set
  VecB = Vec Bool

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

VecB takes a parameter of type Nat 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 : Nat
    vector : VecB ( length )

The followings are examples of value of VR:

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

  vr2 : VR
  vr2 = record { length = succ 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 -> Nat
 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 : Nat
     vec : Vec X len

  vrpNat : VRP Nat
  vrpNat = record { len = succ (succ zero)
                  ; vec = zero :: (succ 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, and furthermore projections are not defined for such fields. Irrelevant fields can only be accessed using pattern matching, as in elimSubset above.

Agda 2.2.10 release notes:

As shown above the axiom irrelevant justifies irrelevant projections. Previously no projections were generated for irrelevant record fields, such as the field certificate in the following record type:

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

Now projections are generated automatically for irrelevant fields (unless the flag --no-irrelevant-projections is used). Note that irrelevant projections are highly experimental.

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

See examples/lattice for an example of how to use the module system and the record types together.

Extending the record module with additional functions

  record A : Set where
    constructor constr
    field 
      n1 : Nat
      n2 : Nat

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

  -- the A record type in action
  a : A
  a = constr zero (succ zero)

  a2 : A
  a2 = A.swap 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 Nat (succ (succ zero))
      l = zero :: (succ zero :: [])
    field
      first : A

Extracting an implicit field:

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

  get : Implicit -> Nat
  get = Implicit.k

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

References

History of changes of the support for records in Agda:

Version-2-2-6:

  • implicit arguments and constructors for records.

Version-2-2-8:

  • pattern matching on records, irrelevant fields

Version-2-2-10:

  • projections generated automatically for irrelevant fields
Page last modified on April 26, 2019, at 01:03 pm
Powered by PmWiki