{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch
Lecture 3: Error propagation in Agda
Haskell is supposed to be a pure functional programming langauge but
in reality it isn't pure but features at least two effects: error
and divergence. Errors arise when we use incomplete patterns as in
the implementation of !! in the Haskell prelude.
In contrast Agda is pure and error propagation has to be made
explicit using the Maybe monad. In this lecture we look at the
insert function as an example of how to implement error propagation
in Agda.
-}
module l03 where
open import Data.Nat
open import Data.List
open import Data.Maybe
{- In the previous lecture we used Maybe to handle errors
when accessing the nth element of a list: -}
_!!_ : {A : Set} → List A → ℕ → Maybe A
[] !! n = nothing
(a ∷ as) !! zero = just a
(a ∷ as) !! suc n = as !! n
{- A more interesting example is the insert operation
which inserts a list at the nth position, e.g.
insert (1 ∷ 2 ∷ 3 ∷ []) 1 (5 ∷ 6 ∷ [])
= just (1 ∷ 5 ∷ 6 ∷ 2 ∷ 3 ∷ [])
-}
insert : {A : Set} → List A → ℕ → List A → Maybe (List A)
insert as zero bs = just (bs ++ as)
insert [] (suc n) bs = nothing
{- In Haskell we would just write
insert (a ∷ as) (suc n) bs = insert as n bs
but in Agda we have to implement error propagation explicitely.
We are using the 'with' construct to pattern match over a
recursively computed result. -}
insert (a ∷ as) (suc n) bs with insert as n bs
insert (a ∷ as) (suc n) bs | just cs = just (a ∷ cs)
insert (a ∷ as) (suc n) bs | nothing = nothing
{- We are exploiting here the fact that Maybe is a monad which
can be used to simulate computations with error. -}