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
    r₁ : Bool
    r₂ : 

Record value definitions

An example:

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

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 2

Agda provides this definition to us with the following syntax:

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

x″ = r′ true 2

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:

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.


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ℕ
    length : 
    vector : Vec  length

list : Listℕ
list = Lℕ 3 (0  1  2  [])

list′ : Listℕ
list′ = Lℕ _ (0  1  2  [])

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


Define Σ with record!

Implicit record fields



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} _≡_


Define the predicate of being a semigroup!

Prove that is a semigroup with _+_!