I have been looking for a programming language to practice dependent type with. During the WG 2.1 meeting, my attention was brought to Agda (in fact, Adga 2). The word Agda may refer to both the proof assistant and its input language. It has been under long development, is relatively matured, has good library support. It supports real dependent type, and, pardon me for my personal preference, it is Haskell-like. So far it seems like a perfect choice.

So, here is my first Agda program. I am merely repeating some simple exercises on lists, which I tried using Haskell in a previous entry Developing Programs and Proofs Spontaneously using GADT.

```
> open import Logic.Identity
> open import Data.Bool
> open import Data.Nat
> open import Data.Nat.Properties
> module Main where
```

### List Concatenation

Adga has natural numbers defined in `Data.Nat`

. With `Nat`

, one can define lists indexed by their lengths as:

```
> data List (a : Set) : Nat -> Set where
> [] : List a zero
> _::_ : {n : Nat} -> a -> List a n -> List a (suc n)
```

The definition of `append`

naturally follows:

```
> append : {a : Set} -> {m , n : Nat} ->
> List a m -> List a n -> List a (m + n)
> append [] ys = ys
> append (x :: xs) ys = x :: append xs ys
```

### List Reversal

Unlike in Haskell, identifiers in Adga have to be defined earlier in the file before they can be referred to. In the usual definition of linear-time list reversal using an accumulating parameter, the recursive call yields a list of length `m + suc n`

. I have got to somehow provide a proof that it equals `suc m + n`

.

How does one provide such a proof? In Omega, one would make a list of all lemmas needed in a `where`

clause and the compiler would mysteriously figure out a way to use them. (Well, I am sure it is well documented. I just have not understood its algorithm.) I would like to have more control over what is happening, and therefore would prefer to present the proof as a type cast from `f (m + suc n)`

to `f (suc m + n)`

for arbitrary type functor `f`

. This is what one would do in Epigram and Adga.

```
psuc : {m : Nat} -> {n : Nat} -> {f : Nat -> Set} ->
f (m + suc n) -> f (suc m + n)
psuc {zero} {n} {f} xs = xs
psuc {suc m} {n} {f} xs = psuc {m} {n} {f'} xs
where f' : Nat -> Set
f' n = f (suc n)
```

At this point I did not yet know that I could use the lemmas defined in `Data.Nat.Properties`

instead of rolling my own. The function `revcat`

can then be defined as below:

```
revcat : {a : Set} -> {m n : Nat} ->
List a m -> List a n -> List a (m + n)
revcat {a} {zero} {n} [] ys = ys
revcat {a} {suc m} {n} (x :: xs) ys =
psuc {m} {n} {List a} (revcat xs (x :: ys))
```

One thing I have yet to figure out is how much of the type information can be inferred. The first clause can be simplified to `revcat [] ys = ys`

. If I omit the type information in the right-hand side of the second clause:

```
revcat {a} {suc m} {n} (x :: xs) ys =
psuc (revcat xs (x :: ys))
```

I would expect Agda to tell me that it cannot infer the types. However, the program still appears to typecheck. When I try to execute `revcat (1 :: (3 :: [])) (2 :: (4 :: []))`

in the interpreter, I get `_86 1 1 (3 :: []) (2 :: (4 :: []))`

, which seems to be an unevaluated expression. Does it not violate the slogan that “well-typed programs don’t go wrong?”

Using the predefined lemma in `Data.Nat.Properties`

:

```
+suc : (n m : Nat) -> n + suc m ≡ suc (n + m)
+suc zero m = refl
+suc (suc n) m = cong suc (+suc n m)
```

The type cast in `revcat`

can be performed using `subst`

:

```
> revcat : {a : Set} -> {m n : Nat} ->
> List a m -> List a n -> List a (m + n)
> revcat {a} {zero} {n} [] ys = ys
> revcat {a} {suc m} {n} (x :: xs) ys =
> subst (List a) (sym (+suc m n)) (revcat xs (x :: ys))
```

### Merging

Once I got `revcat`

working, `merge`

is not too difficult.

```
> merge : {m n : Nat} ->
> List Nat m -> List Nat n -> List Nat (m + n)
> merge [] ys = ys
> merge {suc m} {zero} (x :: xs) Nil =
> subst (List Nat) (+zero (suc m)) (x :: xs)
> merge {suc m} {suc n} (x :: xs) (y :: ys) =
> if x < y then
> x :: merge xs (y :: ys)
> else (y ::
> subst (List Nat) (+suc m n) (merge (x :: xs) ys))
```

Curiously, the parentheses around the `else`

branch can not be omitted. Without them the expression would be parsed as `(if ... then .. else y) :: subst...`

. The precedence for `_::_`

, which is not declared, is assumed to be higher than `if_then_else_`

.

### Balanced Trees

I tried to go on to define balanced trees, like in Altenkirch, McBride, and McKinna’s introduction to Epigram:

```
data Parity : Set where
Even : Parity
Odd : Parity
parity : Parity -> Nat
parity Even = 0
parity Odd = 1
data Tree (a : Set) : Nat -> Set where
Nul : Tree a zero
Tip : a -> Tree a (suc zero)
Bin : {m n : Nat} -> (p : Parity) ->
Tree a (parity p + n) -> Tree a n -> Tree a (parity p + (n + n))
```

The `Bin`

constructor needs a parity bit. If the parity bit is `Even`

, the two subtrees have the same size. Otherwise they differ by one.

However, I have not figured out how to pattern match the size parameter: when defining a function `f : {a :Set} -> {n : Nat} -> Tree a n-> ...`

, Agda complained when I tried this pattern `f {a} {n} (Bin Odd t u) = ...`

because `parity p + (n' + n') != n`

. Perhaps I should start reading some more documents.