Continuing with my Adga programming practice. This time I am implementing the example in another section of Why Dependent Types Matter by Altenkirch, McBride, and McKinna in Agda: proving that mergesort returns an ordered list.
> module Main where
> open import Prelude
> open import Data.Nat hiding (_≤_)
> open import Data.List
Order
To begin with, a term of type m ≤ n
is a proof that a natural number m
is at most n
:
> data _≤_ : Nat -> Nat -> Set where
> le0 : {n : Nat} -> zero ≤ n
> le1 : {m n : Nat} -> m ≤ n -> (1 + m) ≤ (1 + n)
An auxiliary function weaken
, which I will need later, weakens a proof of (1+m) ≤ n
to a proof of m ≤ n
:
> weaken : {y x : Nat} -> (1 + y) ≤ x -> y ≤ x
> weaken (le1 le0) = le0
> weaken (le1 (le1 p)) = le1 (weaken (le1 p))
Given two natural numbers m
and n
, the function order
, to be defined later, determines their order by returning a proof. The proof has to be wrapped in a datatype Order
:
> data Order : Nat -> Nat -> Set where
> leq : {m n : Nat} -> m ≤ n -> Order m n
> gt : {m n : Nat} -> (1 + n) ≤ m -> Order m n
Agda does not provide a generic case
expression, so I have to define my own for Order
:
> caseord : {m n : Nat} {a : Set} -> Order m n
> -> ((m ≤ n) -> a) -> (((1 + n) ≤ m) -> a) -> a
> caseord (leq p) f g = f p
> caseord (gt p) f g = g p
The function order
can thus be defined by:
> order : (m : Nat) -> (n : Nat) -> Order m n
> order zero n = leq le0
> order (suc m) zero = gt (le1 le0)
> order (suc m) (suc n) =
> caseord (order m n) (leq ∘ le1) (gt ∘ le1)
Ordered List
There are many ways one can express the property that a list is sorted. The choice depends on what one needs for the proof. To prove that merge
sorts the list, Altenkirch, McBride, and McKinna suggests the following “external bound” representation of sortedness:
> data OList : Nat -> Set where
> Nil : {b : Nat} -> OList b
> Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
The datatype OList b
represents a sorted list of natural numbers whose elements are all greater than or equal to the bound b
. The bound, however, is supplied externally and need not be precise. Every sorted list of natural numbers has type OList 0
, for instance. The Cons
constructor demands that the newly added element x
is bounded by the externally supplied bound b
, and that the tail can be bounded by x
.
Merging Sorted Lists
With OList
, merge
can be verified very easily:
> merge : {b : Nat} -> OList b -> OList b -> OList b
> merge Nil ys = ys
> merge xs Nil = xs
> merge (Cons x blex xs) (Cons y bley ys) =
> caseord (order x y)
> (\\ xley -> Cons x blex (merge {x} xs (Cons y xley ys)))
> (\\ pylex -> Cons y bley (merge {y} (Cons x (weaken pylex) xs) ys))
Note, for example, that Cons y bley ys : OList b
is updated to Cons y xley ys : OList x
simply by using a different proof.
Mergesort
The rest are just some routine code: dealing elements to a tree, and perform successive merging by a fold on the tree. Mergesort is defined by mergeT ∘ dealT
. The code below is similar to that in my previous blog entry, but without the size constraint.
> data Parity : Set where
> Even : Parity
> Odd : Parity
> data Tree (a : Set) : Set where
> Nul : Tree a
> Tip : a -> Tree a
> Bin : Parity -> Tree a -> Tree a -> Tree a
> foldT : {a b : Set}
> -> (Parity -> b -> b -> b)
> -> (a -> b)
> -> b
> -> Tree a -> b
> foldT f g e Nul = e
> foldT f g e (Tip x) = g x
> foldT f g e (Bin p t u) = f p (foldT f g e t) (foldT f g e u)
> insert : {a : Set} -> a -> Tree a -> Tree a
> 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 x (Bin Odd t u) =
> Bin Even t (insert x u)
> dealT : List Nat -> Tree Nat
> dealT = foldr insert Nul
> mergeT : Tree Nat -> OList 0
> mergeT = foldT (\p xs ys -> merge xs ys)
> (\x -> Cons x le0 Nil)
> Nil
> msort : List Nat -> OList 0
> msort = mergeT ∘ dealT
newsh (sorry for the late response),
I think OList is a sorted list. Consider xs : OList 0. If xs is Nil, it is sorted. If xs equals, say, Cons 3 0≤3 ys, the tail ys must have type OList 3. Thus ys is lower-bounded by 3, not 0.
I think this only proves that the resulting list has a lower bound. You can construct arbitrary (unordered) lists of type (OList 0). The only restriction is that all elements are >= 0 (which is true by the definition of >=).