My Weblog

Blog about programming and math

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))))))).

Advertisements

February 10, 2013 - Posted by | Agda, Programming |

No comments yet.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: