{- Now records. -} module Records where open import Data.Unit using (⊤; tt) open import Data.Bool -- Records are just Σ-types. So here's Σ: record Σ (A : Set)(B : A → Set) : Set where field fst : A snd : B fst -- Building record values ex : Σ Bool T ex = record { fst = true; snd = tt } {- What about accessing the fields? There are two ways one might want to do this: • Projection, for instance using projection functions fst : ∀ {A B} → Σ A B → A snd : ∀ {A B}(p : Σ A B) → B (fst p) • Opening, given p : Σ A B we might want to open p to get fst : A snd : B fst Using the module system we can get both! For each record you get a parameterized module containing projection functions: record R : Set where field x₁ : A₁ x₂ : A₂ [x₁] ... xn : An [x₁..xn-1] module R (r : R) where x₁ : A₁ x₂ : A₂ [x₁] ... xn : An [x₁..xn-1] -} -- Doing C-c C-o Σ to see the contents of the Σ module gives us: -- Modules -- Names -- fst : {A : Set} {B : A → Set} → Σ A B → A -- snd : {A : Set} {B : A → Set} (r : Σ A B) → B (Σ.fst r) -- We can also instantiate it to a particular record value: open Σ ex renaming (fst to x; snd to y) -- now x = true : Bool and -- y = tt : ⊤ -- Let's return to the sort example. -- We can pack up a set and a comparison function -- in a Poset record. record Poset : Set₁ where field A : Set _≤_ : A → A → Bool -- Definitions inside a record go in the record module. _≥_ : A → A → Bool x ≥ y = y ≤ x op : Poset op = record { _≤_ = _≥_ } -- C-c C-o Poset gives us -- Modules -- Names -- _≤_ : (r : Poset) → Poset.A r → Poset.A r → Bool -- _≥_ : (r : Poset) → Poset.A r → Poset.A r → Bool -- A : Poset → Set -- op : (r : Poset) → Poset open import Data.List -- Our sort module is now parameterized on a Poset record (not the module). module Sort (P : Poset) where -- This is a good example of where opening a record is really nice. open Poset P insert : A → List A → List A insert y [] = y ∷ [] insert y (x ∷ xs) = if y ≤ x then y ∷ x ∷ xs else x ∷ insert y xs sort : List A → List A sort [] = [] sort (x ∷ xs) = insert x (sort xs) open import Nat NAT : Poset NAT = record { _≤_ = _≤_ } -- the A field can be inferred from _≤_ -- We now instantiate with the NAT poset. open Sort NAT -- Now sort : List ℕ → List ℕ xs = 3 ∷ 7 ∷ 0 ∷ 10 ∷ 2 ∷ [] test₁ = sort xs