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

## 1 The Con of Agda.

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

## 2 The Pro of Agda.

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

## 3 Define your own Nature number

1. Space between operator and operands in Agda

```3::[] -- wrong
3 :: [] -- right
```
2. Nature number can be defined as 0, (0 + 1), (0 + 1 + 1), ⋯ etc. ∀ a ∈ ℕ ∣ suc a ∈ ℕ
3. 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
```
4. In Agda

```data Nat : Set where
zero : Nat
suc : Nat → Nat

add Nat → Nat → Nat

-- operator
_+_ : Nat → Nat
zero + zero = zero
zero + b = b
(suc a) + b = suc (a + b)
```
5. 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 *`
6. Define a list in Agda

```data List (A : Set) : Set where
[] : A
_::_ : A → List A → List A
```
7. 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`
8. 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 *`
9. 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::[a] -> Maybe a
```

```head : {A : Set} -> List A -> Maybe A
head (x :: cs) = just x
```
12. length function in Agda

```length : {A : Set} -> List A -> ℕ
length [] = zero
length (x :: cs) = suc (length cs)
```
13. 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
```
14. Concate String in Agda

• It is from standard library
```"dog" ++ "cat"
```
15. Convert number to String

```show 2
```
16. Write String to file

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

Created: 2021-09-22 Wed 17:21

Validate