#+HTML_HEAD: *** What is Agda?

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. Nature number can be defined as 0, (0 + 1), (0 + 1 + 1), ⋯ etc. ∀ a ∈ ℕ ∣ suc a ∈ ℕ
2. 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)

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

4. 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 *
5. Define a list in Agda

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

6. 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
7. 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 *
8. 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 [] = Nothing
head x:cs = Just x

10. head function in Agda

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

11. length function in Agda

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

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

Created: 2019-08-03 Sat 16:03

Validate