After the Agda Records Tutorial

module Sets.Records where

open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality using (_≡_)
import Relation.Binary.PropositionalEquality as Eq

Record set definitions

A record type is a special set for representing tuples of values. For example, the following set represents a Bool, ℕ pair:

record R : Set where
  field
    r₁ : Bool
    r₂ : ℕ

Record value definitions

An example:

x : R
x = record { r₁ = true; r₂ =  }

Record value definitions with constructors

One could define a constructor for R values:

r : Bool → ℕ → R
r b n = record { r₁ = b; r₂ = n }

x′ = r true 

Agda provides this definition to us with the following syntax:

record R′ : Set where
  constructor r′   -- record constructor
  field
    r₁ : Bool
    r₂ : ℕ

x″ = r′ true 

Field selectors

Agda defines field selectors automatically:

sel₁ : R → Bool
sel₁ = R.r₁

sel₂ : R → ℕ
sel₂ = R.r₂

x‴ = r (R.r₁ x) (R.r₂ x)

record vs. data definitions

For every set defined with record there is an equivalent set defined with data.

For example, the following set is equivalent to R:

data R″ : Set where
  r″ : (r₁ : Bool) (r₂ : ℕ) → R″ 

r₁ : R″ → Bool
r₁ (r″ a b) = a

r₂ : R″ → ℕ
r₂ (r″ a b) = b

Records have the following advantages over data definitions:

• We get selector functions for free.
• A record is definitionally equivalent to its recombined parts:

extRec : (x : R) → x ≡ r (R.r₁ x) (R.r₂ x)
extRec _ = Eq.refl

-- {- not possible -}
-- extData : (x : R″) → x ≡ r″ (r₁ x) (r₂ x)
-- extData _ = refl

It is advised to use record definitions whenever it is possible.

Exercises

• Define ⊤ as a record!
• Define _×_ as a record!

Dependent records

The type of a field can depend on the values of the previous fields.

For example the following set is equivalent to List ℕ:

open import Data.Vec using (Vec; []; _∷_)

record Listℕ : Set where
  constructor Lℕ
  field
    length : ℕ
    vector : Vec ℕ length

list : Listℕ
list = Lℕ  ( ∷  ∷  ∷ [])

list′ : Listℕ
list′ = Lℕ _ ( ∷  ∷  ∷ [])

The type of the selector functions:

length′ : Listℕ → ℕ 
length′ = Listℕ.length

vector′ : (x : Listℕ) → Vec ℕ (length′ x)   -- dependent
vector′ = Listℕ.vector

Parameterised record

The previous example parameterised with the types of the vector elements:

record List (A : Set) : Set where
  constructor L
  field
    length : ℕ
    vector : Vec A length

list₂ : List Bool
list₂ = L _ (true ∷ false ∷ true ∷ [])

The type of the selector functions:

length″ : {A : Set} → List A → ℕ 
length″ = List.length

vector″ : {A : Set} (x : List A) → Vec A (length″ x)   -- dependent
vector″ = List.vector

Note that the parameters became implicit in the field selectors' type.
(This is a design decision of the Agda language.)

Exercises

Define Σ with record!

Implicit record fields

TODO

Exercise

Define the predicate of being an equivalence relation!

record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where

Prove that _≡_ is an equivalence relation on any set!

isEquivalence : {A : Set} → IsEquivalence {A} _≡_

Exercise

Define the predicate of being a semigroup!

Prove that ℕ is a semigroup with _+_!