Records.agda

{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007


                   Agda

                Ulf Norell

-}

-- Records are labeled sigma types.

module Records where

open import Nat
open import Bool

{-

  A very simple record.

-}

record Point : Set where
  field
    x : Nat
    y : Nat

-- A record can be seen as a one constructor datatype. In this case:
data Point' : Set where
  mkPoint : (x : Nat)(y : Nat) -> Point'

-- There are a few differences, though:

-- To construct a record you use the syntax record { ..; x = e; .. }
origin : Point
origin = record { x = 0; y = 0 }

-- instead of
origin' : Point'
origin' = mkPoint 0 0

-- What's more interesting is that you get projection functions
-- for free when you declare a record. More precisely, you get a module
-- parameterised over a record, containing functions corresponding to the
-- fields. In the Point example you get:
{-
  module Point (p : Point) where
    x : Nat
    y : Nat
-}

-- So Point.x : Point -> Nat is the projection function for the field x.
getX : Point -> Nat
getX = Point.x

-- A nifty thing with having the projection functions in a module is that
-- you can apply the module to a record value, in effect opening the record.
sum : Point -> Nat
sum p = x + y
  where
   open module Pp = Point p

-- The final difference between records and datatypes is that we have
-- η-equality on records.

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

η-Point : (p : Point) -> p == record { x = Point.x p; y = Point.y p }
η-Point p = refl

{-

  The empty record

-}

-- One interesting benefit of this is that we get a unit type with
-- η-equality.
record True : Set where

tt : True
tt = record{}

-- Now, since any element of True is equal to tt, metavariables of
-- type True will simply disappear. The following cute example exploits
-- this:

data False : Set where

NonZero : Nat -> Set
NonZero zero    = False
NonZero (suc _) = True

-- We make the proof that m is non-zero implicit.

_/_ : (n m : Nat){p : NonZero m} -> Nat
(n / zero) {}
zero  / suc m = zero
suc n / suc m = div (suc n) (suc m) m
  where
    div : Nat -> Nat -> Nat -> Nat
    div  zero    zero   c = suc zero
    div  zero   (suc y) c = zero
    div (suc x)  zero   c = suc (div x c c)
    div (suc x) (suc y) c = div x y c

-- Now, as long as we're dividing by things which are obviously
-- NonZero we can completely ignore the proof.

five = 17 / 3

{-

  A dependent record

-}

-- Of course, records can be dependent, and have parameters.
record ∃ {A : Set}(P : A -> Set) : Set where
  field
    witness : A
    proof   : P witness