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.
Sorry for the inconvenience. The color for code was cadetBlue (#5F9EA0). Now its teal (#008080 ). Hope it’s better…
Please change the color of your code to something darker, it is rather illegible on the white background.
Thanks!