Agda
A whirlwind tour through Agda
Agda whitespace rules
Agda allows UNICODE! IN! VARIABLES! so:
i:Int is! not! i : Int
- the first thing is an indentifier of type
i:Int - the second thing is an
iof typeInt
Dependent Type Theories with Agda
booleans
Consider two empty declarations:
data False : Set where
this is a type with nothing in it!
record True : Set where
this is a type with exactly one thing in it!
False has no elements in it, and True has exactly one element in it.
trivial : True
trivial = _
since True only takes on one type, Agda can figure out the wild-card value is unique
isTrue : Bool -> Set
isTrue true = True
isTrue false = False
we have now created True/False AS TYPES. We just mapped values to types.
less than
_<_ : Nat -> Nat -> Bool
and now consider:
_ < zero = false
zero < succ n = true
succ m < succ n = m < n
length of list
length : { A : Set } -> List A -> Nat
length [] = zero
length (x :: xs) = succ (length xs)
safe! list lookup
we leverage the fact that False -> A has no candidates.
lookup : {A : Set}(xs : List A)(n : Nat) -> isTrue (n < length xs) -> A
lookup [] n ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (succ n) p = lookup xs n p
where () is a the “absurd pattern”, and this can’t execute.
and p is a proof that we show to Agda that (n < length xs).
standard datatypes
Set is the type of all small types (level 0 types in).
bool
data Bool : Set where
false : Bool
true : Bool
not: Bool -> Bool
not false = true
not true = false
numbers
data Nat : Set where
zero : Nat
succ : Nat -> Nat
plus : Nat -> Nat -> Nat
plus zero m = m
plus (succ n) m =
succ (plus n m)
notice that succ in this case is a function because in a Dependent Type Theories our data type can return other stuff.
Some rules about pattern matching….
- patterns must be exaustive (every case must be covered)
- patterns must be disjoint — they cannot overlap in what they match (i.e. other languages have some matching order)
infix operators
_op_ is the way that infix operators are defined, so:
_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)
also that underscores represents where arguments can go, so if, then, else can be written as if_then_else_
List
data List (A : Set) : Set
where
[] : List A
_::_ : A -> List A -> List A
indexed type
data Eq {A : Set} (x : A) : A -> Set where
refl : Eq x x
this is an indexed type, meaning the type of the data type is a function from A to a type in Set.
This means that there is a different type for every value of x.
example proof
we want to prove “if m = n, then f m = f n”
cong : {A : set} {B : set} {m : A} {n : A} (f: A -> B) -> Eq m n -> Eq (f m) (f n) cong f refl = reflthe key note that the left refl has a type
Eq m n, the right refl is implicitly defined through consideringEq
let + where
trip : Nat -> Nat
trip n =
let double = n + n
triple = n + double
in triple
lambda
addZero : Nat -> Nat
addZero n = (\x -> x + zero) n
polymorphic types
identity : (A : Set) -> A -> A
identity A x = x
and now you can make identity things such as:
zero' : Nat
zero' = identity Nat zero
you will note that the polymorphism is explicitly instantiated (type inference is not figured out for you, you said A is of a particular argument explicitly).
polymorphic types, implicitly
obviously Agda can guess what the types of things are. So:
identity : {A : Set} -> A -> A
identity x = x
and then you can write:
zero '' : Nat
zero'' = identity Zero
you will note that subsequent type instantiation is now implicit.
records
record Position : Set where
field
xc : Nat
yc : Nat
you can create instances of this record
pos : Position
pos = record { xc = zero; yc = succ(zero) }
along with the record constructor, you get selectors for each field (Position.xc etc…) defined for you:
myxc : Position -> Nat
myxc p = Position.xc p
myyc : Position -> Nat
myyc p = Position.yc p
our record constructors could have parameters, so:
record Position : Set (A : Set) (B : Set) where
field
xc : A
yc : B
and then you can create constructors with annotated types
pos : Position Nat Nat
pos = record { xc = zero; yc = succ(zero) }