## 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

No comments yet.

## Leave a Reply