‎

1. The Con of Agda.
2. The Pro of Agda.
3. Define your own Nature number

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

Space between operator and operands in Agda
```
3::[] -- wrong
3 :: [] -- right
```
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)

  -- operator
  _+_ : Nat → Nat
  zero + zero = zero
  zero + b = b
  (suc a) + b = suc (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 Maybe
```
data 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 Haskell

head::[a] -> Maybe a
head [] = Nothing
head x:cs = Just x

head function in Agda

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

length function in Agda

length : {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

Concate String in Agda
- It is from standard library
```
"dog" ++ "cat"
```
Convert number to String
```
show 2
```

Write String to file

-- write Integer to file
writeFile "/tmp/f.x"  (show 2)
-- write string to file
writeFile "/tmp/f.x" "dog"

Table of Contents

1 The Con of Agda.

2 The Pro of Agda.

3 Define your own Nature number