{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 4: Dependent types

  Instead of propagating errors at runtime we'd rather avoid them. In
  this lecture we show how dependent types can be used to implement an
  error-free version of !! using Vec (Vactors) and Fin (finite types)
  in Agda.

-}
module l04 where

open import Data.Nat

{- We define the type of Vectors where Vec A n is the n tuples of As
   or equivalently lists over A of length n. Indeed we are using the
   same construtors as for lists (Agda allows constructor overloading).
-}
data Vec (A : Set) : ℕ → Set where 
  [] : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

infixr  _∷_

{- In future we will use the standard library:
   open import Data.Vec -}

-- some example vectors:
l1 : Vec ℕ 
l1 =  ∷  ∷  ∷ []

l2 : Vec ℕ 
l2 =  ∷  ∷ []

{- We reimplement append for Vectors: 
   Note that the code is the same as for lists only the type is
   different, indeed more informative. -}
_++_ : {A : Set} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ as ++ bs


{- To define an error-free version of !! we need to restrict the index
   set to a finite set of size n. I.e. we define the family
    Fin : ℕ → Set
   such that 
    Fin 0 = {}
    Fin 1 = { 0 }
    Fin 2 = { 0 , 1 }
    Fin 3 = { 0 , 1 , 2 }
    ...

   Indeed Fin is related to the natural numbers and has the same
   constructors but with different types.
-}

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n) 
  suc : {n : ℕ} → Fin n → Fin (suc n)

{- Examples for Fin -}
i1 : Fin 
i1 = zero{zero}

i2 : Fin 
i2 = suc{suc zero} i1

{- we can now implement a total version of !!  Note that the bad case
   is now impossible, since there is no element of Fin 0. Agda can
   recognize this and marks the impossible pattern with (). -}
_!!_ : {A : Set} → {n : ℕ} → Vec A n → Fin n → A
[] !! ()
(a ∷ as) !! zero = a
(a ∷ as) !! suc n = as !! n


{- To illustrate finite sets and getting used to dependent types we
   define some basic functions on Fin -}

{- max returns the maximial element in a non-empty finite set: -}
max : {n : ℕ} → Fin (suc n)
max {zero} = zero
max {suc n} = suc (max {n}) 

{- emb embeds Fin n into Fin (n+1). 
   e.g. emb {2} (suc{1} zero{0}) = suc{2} zero{1}
-}
emb : {n : ℕ} → Fin n → Fin (suc n)
emb zero = zero
emb (suc i) = suc (emb i)

{- Finally, we define inv which reverses the order of a
   given finite set. Conveniently it can be defined using max and
   emb. 

   E.g.
   inv {3} 0 = max {3} = 2
   inv {3} 1 = emb (max {1}) = 1
   inv {3} 2 = emb (emb (max {0})) = 0
-}
inv : {n : ℕ} → Fin n → Fin n
inv zero = max
inv (suc i) = emb (inv i)

{- Finally we looked at ++' the reversing version of append.
   Alas, our technique just to change the type but to keep the code
   doesn't work any longer. 

_++'_ : {A : Set} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
as ++' [] = as
as ++' (b ∷ bs) = (b ∷ as) ++' bs

  leads to a type error since Agda claims that n + 0 is not equal to n
  Why is this? The Agda type checker only uses definitional equalities,
  e.g. in the case of + these are
  zero  + n = n
  suc m + n = suc (m + n)
  Other equalities such as n + zero = n require explicit proof. 
-}