Dependently-Typed-Programming-in-Agda.agda

module Dependently-Typed-Programming-in-Agda where

open import Nat
open import Vector
open import List

{- Studying the book Dependently Typed Programming in Agda by Ulf Norell and James Chapman -}

-- A vector containing n copies of an element x
vec : {n : Nat} {A : Set} -> A -> Vector A n
vec {zero}  x = end
vec {suc n} x = (n , x) (vec x)


data SubList {A : Set} : List A -> Set where
  end  : SubList end
  _,_  : forall x {xs} -> SubList xs -> SubList (x , xs)
  skip : forall {x xs} -> SubList xs -> SubList (x , xs)

data Parity : Nat -> Set where
  even : (k : Nat) -> Parity (k * 2)
  odd  : (k : Nat) -> Parity (1 + k * 2)


test-vec : Vector Nat 5
test-vec = vec 2

-- parity : (n : Nat) → Parity n  -- this type is the constructor of Parity
-- parity zero    = even zero
-- parity (suc n) with parity n
-- ... | k →


parity : (n : Nat) -> Parity n
parity zero = even zero
parity (suc n) with parity n
... | even k = odd k  -- a proof that n is even. Now I have to prove that it's successor is odd
... | odd  k = even (suc k)  -- a proof that n is odd

-- Parity works with proofs of half the number. Here we are using parity to get half of a number
half : Nat → Nat
half n with parity n
half .(k * 2)       | even k = k
half .(suc (k * 2)) | odd k  = k

data _belongs-to_ {A : Set} (x : A) : List A -> Set where
  head : ∀ {xs} -> x belongs-to (x , xs)
  tail : ∀ {y xs} -> x belongs-to xs -> x belongs-to (y , xs)

-- Given a proof of x belongs-to xs we can compute the index at which x occurs in xs
-- simply by counting the number of tls in the proof.
index : ∀ {A} {x : A} {xs} -> x belongs-to xs -> Nat
index head     = zero
index (tail p) = suc (index p )