## Table of Contents

- Agda is dependent type language.
- You can use almost any unicode as operator.
- Agda is similar to Haskell, but it is fully dependent type.
- If you know a bit of Haskell, then it is easy to get start.

## 1 The Con of Agda.

- It is painful to install.
- You need Emacs to input those unicode characters.
- You never expect write
**Agda**code on your day job. **Agda**is painfully slow.

## 2 The Pro of Agda.

- You learn some the most fundamental stuff from Agda, e.g define your own
**Nature**number - You can use lots of
**unicode**characters in your code, make your code looks pretty.

## 3 Define your own **Nature** number

- Nature number can be defined as 0, (0 + 1), (0 + 1 + 1), ⋯ etc. ∀ a ∈ ℕ ∣ suc a ∈ ℕ
We can use

**Peano numbers**to represent**Nature number**. Peano numbers need only a zero and a successor function to represent it. In Haskell, we can define as following.data Nat = Zero | Suc Nat add Zero b = b add (Suc a) b = Suc (add a b)

In Agda

data Nat : Set where zero : Nat suc : Nat -> Nat add Nat -> Nat -> Nat add zero b = b add (Suc a) b = Suc (add a b)

Define a list in Haskell

data List a = Nil | Cons a (List a)

`List = []`

is type constructor with`kind * -> kind *`

`List a = [a] ~ is type with ~kind *`

`Nil = []`

is value with polymorphic types`List a`

and`[a]`

respectively`Cons = :`

is value constructor with`kind * -> kind *`

Define a list in Agda

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

- What does it mean for above the code?
`Set`

is type of type in**Agda**`A : Set`

, it means A ∈ Set or A is type of`Set`

`List (A : Set) : Set`

, it means type constructor**List**needs type A is also a Set`_::_`

, it means**append**a element`A`

to a`List A`

and return a`List A`

Let see how to define Maybe in Agda, first, we review

**Haskell**Maybedata Maybe a = Nothing | Just a

`Maybe`

is just**type constructor**with ~kind * -> kind * ~`Noting`

is**value constructor**with type ~kind * ~`Just a`

is**value constructor**with type ~kind * -> kind * ~`Maybe a`

is type with`kind *`

Maybe in Agda

data Maybe (A : Set) : Set where nothing : Maybe A just : A -> Maybe A

`Maybe`

is just**type constructor**with`Set -> Maybe Set`

**head**function in Haskellhead::[a] -> Maybe a head [] = Nothing head x:cs = Just x

**head**function in Agdahead : {A : Set} -> List A -> Maybe A head [] = nothing head (x :: cs) = just x

**length**function in Agdalength : {A : Set} -> List A -> ℕ length [] = zero length (x :: cs) = suc (length cs)

map function in Agda

map {A B : Set} -> (A -> B) -> List A -> List B map f [] = [] map f (x :: cs) = f x :: map f cs