# My Weblog

## Learning Agda

Finally I am feeling bit comfortable with Agda and feeling great :). I started reading Ulf Norell‘s Dependently Typed Programming in Agda. Tutorials on Agda-wiki , AgdaTutorial , papers which mention Agda , stackoverflow post, Introduction to Agda and Programming in Martin-Löf’s Type Theory. I wrote some of the codes from the paper. You can also try a similar language Idris ( See the stackoverflow post about difference between these languages ).

```module Basic where

data Bool : Set where
true : Bool
false : Bool

not : Bool → Bool
not true = false
not false = true

or : Bool → Bool → Bool
or false false = false
or _ _ = true

and : Bool → Bool → Bool
and true true = true
and _ _ = false

data ℕ  : Set where
zero : ℕ
suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + m = m
suc n + m = suc ( n + m )

_⋆_ : ℕ → ℕ → ℕ
zero ⋆ m = zero
suc n ⋆ m =   ( n ⋆ m ) + m

fold-ℕ : ℕ → ( ℕ → ℕ ) → ℕ → ℕ
fold-ℕ u _ zero = u
fold-ℕ u f ( suc n ) = f ( fold-ℕ u f n )

if_then_else_ : { A : Set } → Bool → A → A → A
if true then x else y = x
if false then x else y = y

data List ( A : Set ) : Set where
[] : List A
_::_ : A → List A -> List A

identity : ( A : Set ) → A → A
identity A x = x

zero′ : ℕ
zero′ = identity ℕ zero

apply : ( A : Set ) ( B : A → Set ) → ( ( x : A ) → B x ) → ( a : A ) → B a
apply A B f a = f a

identity₂ : ( A : Set ) → A → A
identity₂ = \A x → x

identity₃ : ( A : Set ) → A → A
identity₃ = \(A : Set ) ( x : A ) → x

identity₄ : ( A : Set ) → A → A
identity₄ = \ ( A : Set ) x → x

id : { A : Set } → A → A
id x = x

true′ : Bool
true′ = id true

one : ℕ
one = identity _ ( suc zero )

_∘_ : { A : Set } { B : A → Set } { C : ( x : A ) → B x → Set }
( f : { x : A } ( y : B x ) → C x y ) ( g : ( x : A ) → B x ) ( x : A )
→ C x ( g x )
( f ∘ g ) x = f ( g x )

plus-two = suc ∘  suc
plus-three = suc ∘ ( suc ∘ suc )

map : { A B : Set } → ( A → B ) → List A → List B
map f [] = []
map f ( x :: xs ) = f x :: map f xs

_++_ : { A : Set } → List A → List A → List A
[] ++ ys = ys
( x :: xs ) ++ ys = x :: ( xs ++ ys )

foldl : { A B : Set } → ( A → B → A ) → A → List B → A
foldl f val [] = val
foldl f val ( x :: xs ) = foldl f ( f val x ) xs

foldr : { A B : Set } → ( A → B → B ) → B → List A → B
foldr f val [] = val
foldr f val ( x :: xs ) = f x ( foldr f val xs )

--type of Vec A is  ℕ → Set. This mean Vec A is family of types indexed by
-- natural numbers

data Vec ( A : Set ) : ℕ →  Set where
[] : Vec A zero
_::_ : { n : ℕ } → A → Vec A n → Vec A ( suc n )

head : { A : Set } { n : ℕ } → Vec A ( suc n )  → A
head ( x :: xs ) = x

vmap : { A B : Set } { n : ℕ } → ( A → B ) → Vec A n → Vec B n
vmap f [] = []
vmap f ( x :: xs ) = f x :: vmap f xs

data Vec₂ ( A : Set ) : ℕ → Set where
nil : Vec₂ A zero
cons : ( n : ℕ ) → A → Vec₂ A n → Vec₂ A ( suc n )
{--
The rule for when an argument should be dotted is:
if there is a unique
type correct value for the argument it should be dotted
--}

vmap₂ : { A B : Set } ( n : ℕ ) → ( A → B ) → Vec₂ A n → Vec₂ B n
vmap₂ .zero f nil = nil
vmap₂ .( suc n ) f ( cons n x xs ) = cons n  ( f x ) ( vmap₂ n f xs )

vmap₃ : { A B : Set } ( n : ℕ ) → ( A → B ) → Vec₂ A n → Vec₂ B n
vmap₃ zero f nil = nil
vmap₃ ( suc n ) f ( cons .n x xs ) = cons n ( f x ) ( vmap₃ n f xs )

pow : ℕ →  ℕ  →  ℕ
pow _  zero = suc zero
pow a ( suc n ) =  a ⋆ pow a n

t : ℕ
t = pow ( suc ( suc  zero ) ) ( suc ( suc ( suc zero ) ) )

```

To evaluate the expression , type C-c C-n. Here is the output of t
suc (suc (suc (suc (suc (suc (suc (suc zero))))))).