*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

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₂ : ℕ

An example:

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

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 field r₁ : Bool r₂ : ℕ x″ = r′ true 2

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`

definitionsFor 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.**

- Define
`⊤`

as a record! - Define
`_×_`

as a record!

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

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

Define `Σ`

with `record`

!

TODO

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

!