Datatypes.agda

{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007


                   Agda

                Ulf Norell

-}

-- This is where the fun begins.
-- Unleashing datatypes, pattern matching and recursion.

module Datatypes where

{-

  Simple datatypes.

-}

-- Let's define natural numbers.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- A simple function.
pred : Nat -> Nat
pred zero    = zero
pred (suc n) = n

-- Now let's do recursion.
_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

infixl 60 _+_

-- An aside on infix operators:
-- Any name containing _ can be used as a mixfix operator.
-- The arguments simply go in place of the _. For instance:

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
-- if false then x else y = y
if_then_else_ false x y = y

{-

  Parameterised datatypes

-}

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

-- The parameters are implicit arguments to the constructors.
nil : (A : Set) -> List A
nil A = [] {A}

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

{-

  Empty datatypes

-}

-- A very useful guy is the empty datatype.
data False : Set where

-- When pattern matching on an element of an empty type, something
-- interesting happens:

elim-False : {A : Set} -> False -> A
elim-False ()  -- Look Ma, no right hand side!

-- The pattern () is called an absurd pattern and matches elements
-- of an empty type.

{-

  What's next?

-}

-- The Curry-Howard isomorphism.
--   CurryHoward.agda