{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Lecture 2: A first taste of Agda In this lecture we start to explore the Agda system, a functional programming language based on Type Theory. We start with some ordinary examples which we could have developed in Haskell as well. -} module l02 where module myNat where {- Agda has no automatically loaded prelude. Hence we can start from scratch and define the natural numbers. Later we will use the standard libray. -} data ℕ : Set where -- to type ℕ we type \bn zero : ℕ suc : (m : ℕ) → ℕ -- \-> or \to {- To process an Agda file we use C-c C-c from emacs. Once Agda has checked the file the type checker also colours the different symbols. -} {- We define addition. Note Agda's syntax for mixfix operations. The arguments are represented by _s -} _+_ : ℕ → ℕ → ℕ zero + n = n suc m + n = suc (m + n) {- Try to evaluate: (suc (suc zero)) + (suc (suc zero)) by typing in C-c C-n -} {- Better we import the library definition of ℕ This way we can type 2 instead of (suc (suc zero)) -} open import Data.Nat {- We define Lists : -} data List (A : Set) : Set where [] : List A _∷_ : (a : A) → (as : List A) → List A {- In future we'll use open import Data.List -} {- declare the fixity of ∷ (type \::) -} infixr 5 _∷_ {- Two example lists -} l1 : List ℕ l1 = 1 ∷ 2 ∷ 3 ∷ [] l2 : List ℕ l2 = 4 ∷ 5 ∷ [] {- implementing append (++) -} _++_ : {A : Set} → List A → List A → List A [] ++ bs = bs (a ∷ as) ++ bs = a ∷ (as ++ bs) {- Note that Agda checks wether a function is terminating. If we type (a ∷ as) ++ bs = (a ∷ as) ++ bs in the 2nd line Agda will complain by coloring the offending function calls in red. -} {- What does the following variant of ++ do ? -} _++'_ : {A : Set} → List A → List A → List A as ++' [] = as as ++' (b ∷ bs) = (b ∷ as) ++' bs {- Indeed it can be used to define reverse. This way to implement reverse is often called fast reverse because it is "tail recursive" which leads to a more efficient execution than the naive implementation. -} rev : {A : Set} → List A → List A rev as = [] ++' as {- We tried to define a function which accesses the nth element of a list: _!!_ : {A : Set} → List A → ℕ → A [] !! n = {!!} (a ∷ as) !! zero = a (a ∷ as) !! suc n = as !! n but there is no way to complete the first line (consider what happens if A is the empty type! -} {- To fix this we handle errors explicitely, using Maybe -} open import Data.Maybe {- This version of the function can either return an element of the list (just a) or an error (nothing). -} _!!_ : {A : Set} → List A → ℕ → Maybe A [] !! n = nothing (a ∷ as) !! zero = just a (a ∷ as) !! suc n = as !! n