Agda Exercise: Sized Mergesort

Continuing with my Adga programming practice. Part of the mergesort example became easy once Max showed me how I should perform the pattern matching in insert.


> open import Prelude
> open import Logic.Identity
> open import Data.Bool
> open import Data.Nat
> open import Data.Nat.Properties

> module Main where

Length-Indexed Lists

Firstly, define length-indexed lists and its fold function.


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

> foldr : {a : Set} -> {n : Nat} -> (b : {m : Nat} -> List a m -> Set)
>           -> ({m : Nat} -> {xs : List a m} 
>                   -> (x : a) -> b xs -> b (x :: xs)) 
>           -> b [] 
>           -> (xs : List a n) -> b xs
> foldr b f e [] = e
> foldr b f e (x :: xs) = f x (foldr b f e xs)

Apart from the extra parameter b, the body of foldr is not too different from the ordinary fold on lists. For genericity, however, its type is more complicated. I wonder whether it is still appropriate to call it a “fold”, now that xs appears as a parameter. Perhaps that is why people talk about “eliminators” rather than folds or catamorphisms.

Size-Indexed Balanced Trees

This is one of the possible ways to define sized-indexed balanced trees. The parity bit keep notes of whether the number of the elements is even or odd.


> data Parity : Set where
>   Even : Parity
>   Odd : Parity

> parity : Parity -> Nat
> parity Even = 0
> parity Odd = 1

The Bin constructor enforces the constraint that if the size is even, the two subtrees must have the same size. Otherwise the left subtree contains exactly one more element than the right.


> data Tree (a : Set) : Nat -> Set where
>   Nul : Tree a 0
>   Tip : a -> Tree a 1
>   Bin : {n : Nat} -> (p : Parity) ->
>           Tree a (parity p + n) -> Tree a n -> Tree a (parity p + (n + n))

Fold on trees is defined in a way similar to fold on lists.


> foldT : {a : Set} -> {n : Nat} -> (b : {m : Nat} -> Tree a m -> Set) 
>           -> ({m : Nat} -> (p : Parity)
>                 -> {t : Tree a (parity p + m)} -> {u : Tree a m}
>                 -> b t -> b u -> b (Bin p t u)) 
>           -> ((x : a) -> b (Tip x))
>           -> b Nul 
>           -> (xs : Tree a n) -> b xs
> foldT b f g e Nul = e
> foldT b f g e (Tip x) = g x
> foldT b f g e (Bin p t u) = f p (foldT b f g e t) (foldT b f g e u)

Mergesort

The function insert adds one element to a balanced tree. I did not know how to get the case for Bin Odd t u type-check until Max pointed out that I could just pattern match the implicit argument {n} of Bin.


> insert : {a : Set} -> {n : Nat} ->
>            a -> Tree a n -> Tree a (suc n)
> insert x Nul = Tip x
> insert x (Tip y) = Bin Even (Tip x) (Tip y)
> insert x (Bin Even t u) =
>    Bin Odd (insert x t) u
> insert {a} x (Bin {n} Odd t u) = 
>    subst (\\ i -> Tree a (suc i)) (sym (+suc n n)) 
>      (Bin Even t (insert x u))

The function dealT, dealing elements of the input list to a balanced tree, can thus be defined as a fold:


> dealT : {a : Set} -> {n : Nat} -> List a n -> Tree a n 
> dealT {a} = foldr (\{m} xs -> Tree a m) insert Nul

The function merge has been discussed before:


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

The merging phase of mergesort can be seen as a fold on a binary tree:

    
> mergeT : {n : Nat} -> Tree Nat n -> List Nat n 
> mergeT  = foldT (\\ {m} t -> List Nat m)
>                 (\\ {m} p xs ys -> 
>                   subst (List Nat) (+assoc (parity p) m m) (merge xs ys))
>                 (\\ x -> x :: [])
>                 []

I needed +assoc to type-cast (parity p + m) + m into parity p + (m + m).

Finally, here comes mergesort.


> msort : {n : Nat} -> List Nat n -> List Nat n 
> msort = mergeT  ∘ dealT

Of course, when it comes to sorting, one would expect that we prove that it actually sorts the list than merely that it preserves the length. It will perhaps be left to the next exercise.

4 thoughts on “Agda Exercise: Sized Mergesort

  1. Dan Piponi

    What are you using for Agda documentation? Where can I find an Agda “hello world” example and the instructions on what I should do with it at the command line once I’ve built agda?

    Reply
  2. Shin Post author

    Dan,

    Adga 2 (which is very different from the previous Agda) is rather new and there are not many written documents yet. However, the “examples” directory in the source distribution contains plenty of library code, sample code, and tutorials. The “examples/Introduction” directory may be a good place to start.

    In dependent type programming, the function append may have taken the place of “hello world.” :)

    If you are familiar with GHCi or Hugs, Agda has a similar command-line interpreter. You have to build the interpreter separately. Type “agda -i -I .agda” to load the file. The interpreter works in a way similar to GHCi or Hugs — “:l” for loading a file, “:r” for reloading, “:q” for quitting, etc.

    But it is recommend to use its Emacs mode instead of the interpreter. It provides more feedback. For example, you can type “?” in place of an expression and Agda tells you what type is expected.

    Reply
  3. Mark

    Interesting stuff but I am also having difficulties getting started. How do you do actually run/develop a program either via the Emacs mode or the interpreter? I’ve been through the Agda wiki and other references but find little to help the beginner. I have some experience using Epigram. Can you help?

    Reply
  4. Shin Post author

    Mark,

    Assuming that you have a source file. Start the Agda interpreter by

    agda -i(path to examples/lib) -I (filename.agda)

    You interact with the interpreter through a traditional read-eval-print loop: you type in an expression, Agda reads it, evals it, and print the result.

    In the Emacs mode, the “Load” command under the Agda menu triggers Agda to parse and type-check the file. Your program is then syntax-highlighted if it succeeds. Otherwise you are shown the error message with the problematic code fragment highlighted. You may need to point Agda to examples/lib, as described in the README file.

    I may not be the right person to answer questions about Agda, since I myself have just started to use it several weeks ago. I believe that people on the Agda mailing list will be very helpful. :)

    Reply

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>