After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. The terminating unfoldr↓ would thus have a simpler type as well as a simpler implemenation:

unfoldr↓ : {a : Set}(b : ℕ -> Set){n : ℕ} ->
    (f : forall {i} -> b (suc i) -> ⊤ ⊎ (a × b i)) ->
      b n -> [ a ]
unfoldr↓ b {zero} f y = []
unfoldr↓ b {suc i} f y with f y
... | inj₁ _ = []
... | inj₂ (x , y') = unfoldr↓ b {i} f y'

The definition passes the termination check, apparently, because unfoldr↓ is defined inductively on n.

To generate a descending a list, one may invent a datatype Wrap that wraps the seed, whose bound is simply the seed itself:

data Wrap : ℕ -> Set where
      W : (n : ℕ) -> Wrap n

The list may then be generated by an unfold:

dec : forall {i} -> Wrap (suc i) -> ⊤ ⊎ (ℕ × Wrap i)
dec {i} (W .(suc i)) = inj₂ (i , W i)

down↓ : ℕ -> [ ℕ ]
down↓ n = unfoldr↓ Wrap dec (W n)


Of course, this would defeat my original goal of reusing the non-dependently typed dec, which is probably a bad idea anyway.

To show that the bound need not be exact, let’s try to generate a descending list whose elements are decremented by 2 in each step. We may use this slightly generalised wrapper:

data Wrap2 : ℕ -> Set where
      W2 : (x : ℕ) -> (bnd : ℕ) -> x ≤ bnd -> Wrap2 bnd

and a function dec2 that decrements a suc i-bounded seed by 2 but showing that the new seed is bounded by i:

dec2 : forall {i} -> Wrap2 (suc i) -> ⊤ ⊎ (ℕ × WAlt i)
dec2 {i} (W2 0 .(1 + i) _) = inj₁ tt
dec2 {i} (W2 1 .(1 + i) _) = inj₁ tt
dec2 {i} (W2 (suc (suc n)) .(1 + i) 2+n≤1+i) =
    inj₂ (n , W2 n i (suc-≤-weaken-l (≤-pred 2+n≤1+i)))


The list can then be unfolded by:

down↓2 : ℕ -> [ ℕ ]
down↓2 n = unfoldr↓ Wrap2 dec2 (W2 n n ≤-refl)

where suc-≤-weaken-l is a proof of forall {m n} -> suc m ≤ n -> m ≤ n.

Unfolding a Tree

It is an easy exercise to come up with a tree version of the unfold above:

unfoldT↓ : {a : Set}(b : ℕ -> Set){n : ℕ} ->
  (f : forall {i} -> b (suc i) -> a ⊎ (b i × b i)) ->
    B n -> Tree a
unfoldT↓ b {0} f y = Nul
unfoldT↓ b {suc i} f y with f y
... | inj₁ x = Tip x
... | inj₂ (y₁ , y₂) =
    Bin (unfoldT↓ b {i} f y₁) (unfoldT↓ b {i} f y₂)

To deal with the second task of building a roughly balanced binary tree, one may try this wrapper:

data Split (a : Set): ℕ -> Set where
  Sp : (xs : [ a ]) -> (bnd : ℕ) ->
    length xs < bnd -> Split a bnd

and try to code up a generator function split↓ having this type:

split↓ : forall {a i} -> Split a (suc i) -> a ⊎ (Split a i × Split a i)


The function split↓ I eventually come up with, however, is much more complicated than I had wished. Even worse, it is now split↓ that fails to pass the termination check.

Ulf Norell suggested some possible fixes. The difficulties, however, is probably a hint that there is something wrong in my approach in the first place. Rather than trying to fix it, Nils Anders showed me how he would tackle the problem from the beginning.

Using Well-Founded Recursion

Nils Anders showed me how to define unfoldT↓ using well-founded recursion. For a simplified explanation, the Standard Library provides a function <-rec having type (after normalisation):

<-rec : (P : ℕ -> Set) ->
  (f : (i : ℕ) -> (rec : (j : ℕ) -> j <′ i -> P j) -> P i) ->
    (x : ℕ) -> P x

With <-rec one can define functions on natural numbers by recursion, provided that the argument strictly decreases in each recursive call. P is the type of the result, parameterised by the input. The function f is a template that specifies the body of the recursion which, given i, computes some result of type P i. The functional argument rec is supposed to be the recursive call. The constraint j <′ i, however, guarantees that it accepts only inputs strictly smaller than i (the ordering <′ is a variation of < that is more suitable for this purpose). One may perhaps think of <-rec as a fixed-point operator computing the fixed-point of f, only that f has to take i before rec because the latter depends on the former.

Let us try to define an unfold on trees using <-rec. The "base-functor" of the datatype Tree⁺ a is F b = a ⊎ b × b. One of the lessons we have learnt is that it would be more convenient for the generating function to return the bound information. We could use a type like this:

F a b k = a ⊎ ∃ (ℕ × ℕ) (\(i , j) -> b i × b j × i <′ k × j <′ k)

But it is perhaps more reader-friendly to define the base functor as a datatype:

data Tree⁺F (a : Set) (b : ℕ -> Set) : ℕ -> Set where
  tip : forall {k} -> a -> Tree⁺F a b k
  bin : forall {i j k} ->
      b i -> b j -> i <′ k -> j <′ k -> Tree⁺F a b k


The generating function for the unfold should thus have type forall {a b i} -> b i -> Tree⁺F a b i.

The function unfoldT↓F is the template for unfoldT↓:

unfoldT↓F : {a : Set} {b : ℕ -> Set} ->
  (f : forall {i} -> b i -> Tree⁺F a b i) ->
   (n : ℕ) -> ((i : ℕ) -> i <′ n -> b i -> Tree⁺ a) ->
    b n -> Tree⁺ a
unfoldT↓F f n rec y with f y
... | tip a = Tip⁺ a
... | bin {i} {j} y₁ y₂ i<n j<n =
    Bin⁺ (rec i i<n y₁) (rec j j<n y₂)


Now unfoldT↓ can be defined by:

unfoldT↓ : {a : Set} {b : ℕ -> Set} ->
  (f : forall {i} -> b i -> Tree⁺F a b i) ->
    forall {n} -> b n -> Tree⁺ a
unfoldT↓ {a}{b} f {n} y =
    <-rec (\n -> b n -> Tree⁺ a) (unfoldT↓F f) n y

All the definition above makes no recursive calls. All the tricks getting us through the termination check are hidden in <-rec. How is it defined?

Well-Founded Recursion Defined on <′

Currently, well-founded recursion are defined in Induction and its sub-modules. They are very interesting modules to study. The definitions there, however, are very abstract. To understand how <-rec works, let's try to implement our own.

This is the definition of <′ from Data.Nat:

data _≤′_ : Rel ℕ where
≤′-refl : forall {n} -> n ≤′ n
≤′-step : forall {m n} -> m ≤′ n -> m ≤′ suc n

_<′_ : Rel ℕ m <′ n = suc m ≤′ n

Recall that the recursion template f has type forall i -> (forall j -> j <′ i -> P j) -> P i. That is, given i, f computes P i, provided that we know of a method to compute P j for all j <′ i. Let us try to construct such a method using f. The function guard f i computes f, provided that the input is strictly smaller than i:

guard : {P : ℕ -> Set} ->
   (forall i -> (forall j -> j <′ i -> P j) -> P i) ->
      forall i -> forall j -> j <′ i -> P j
guard f zero _ ()
guard f .(suc j) j ≤′-refl = f j (guard f j)
guard f (suc i) j (≤′-step j<i) = guard f i j j<i

Observe that guard terminates because it is defined inductively on i. If we discard the type information, all what guard f i j is to make a call to f j. Before doing so, however, it checks through the proof to make sure that j is strictly smaller than i. In f j (guard f j), the call to guard f j ensures that subsequent calls to f are given arguments smaller than j.

Now <-rec can be defined by:

<-rec : (P : ℕ -> Set) ->
   (forall i -> (forall j -> j <′ i -> P j) -> P i) ->
      forall n -> P n
<-rec P f n = f n (guard f n)

In Induction.Nat, <-rec is an instance of well-founded recursion defined using the concept of accessibility, defined in Induction.WellFounded. I find them very interesting modules about which I hope to understand more.

To be continued...

The AoPA(Algebra of Programming in Agda) library allows one to derive programs in a style resembling that in the book Algebra of Programming in Agda. For example, the following is a derivation of insertion sort:

sort-der : ∃ ([ Val ] -> [ Val ]) (\f -> ordered? ○ permute ⊒ fun f )
sort-der = exists (
  ⊒-begin
      ordered? ○ permute
  ⊒⟨ (\vs -> ·-monotonic ordered? (permute-is-fold vs)) ⟩
      ordered? ○ foldR combine nil
  ⊒⟨ foldR-fusion ordered? ins-step ins-base ⟩
      foldR (fun (uncurry insert)) nil
  ⊒⟨ foldR-to-foldr insert [] ⟩
      fun (foldr insert [])
  ⊒∎)

isort : [ Val ] -> [ Val ]
isort = witness sort-der


The type of sort-der is a proposition that there exists a program of type [ Val ] → [ Val ] that is contained in ordered ? ◦ permute, a relation mapping a list to one of its ordered permutations. The combinator fun embeds a function in a relation. Relations on each line are related by relational inclusion (⊒), while the proof of inclusion are given in angle brackets. In the final step, the relation foldR (fun (uncurry insert)) nil is refined to a function using the rule:

foldR-to-foldr : {A B : Set} -> (f : A -> B -> B) -> (e : B) ->
    foldR (fun (uncurry f)) (singleton e) ⊒ fun (foldr f e)


which says that a relational fold is a functional fold if the algebra (f) is a function. When the proof is completed, an algorithm isort is obtained by extracting the witness of the proposition. It is an executable program that is backed by the type system to meet the specification.

One may wonder: why insertion sort, rather than something more interesting such as mergesort or quicksort? Because we have not yet figured out how to properly deal with hylomorphism yet. One of the things still missing in AoPA is a treatment of unfolds. AoPA attempts to model the category of sets and relations. In this context one can talk about unfolds because they are simply the converses of folds. We perform the derivations in terms of folds, and refine the converse of a relational fold to a functional unfold provided that the coalgebra is a function:

foldR˘-to-unfoldr : {A B : Set} -> (f : B -> ⊤ ⊎ (A × B)) ->
    (foldR ((fun f) ˘ ○ (fun inj₂)) (\b -> isInj₁ (f b))) ˘ ⊒ fun (unfoldr f)


where ˘ denotes relational converse and unfoldr is given by the usual definition (one that a Haskell programmer would expect, modulo syntax):

unfoldr : {A B : Set} -> (B -> ⊤ ⊎ (A × B)) -> B -> [ A ]
unfoldr f b with f b
... | inj₁ _ = []
... | inj₂ (a , b') = a ∷ unfoldr f b'

The only problem is that this unfoldr cannot pass the termination check of Agda.

My first thought was to wait until Agda supports codata and coinduction. However, the reason I wanted an unfold in AoPA in the first place was to compose it with a fold to form a hylomorphism, which is not allowed if the unfold returns codata. I then attempted to model unfolds in a way similar to what we did in relational program derivation. We know that the recursive equation:

$R\; =\; S\; ○$FR ○ T

$$

has a unique solution R = ⦇S⦈ ○ ⦇T⦈˘ if and only if T is well-founded. In program derivation, the proof of well-foundedness is usually given separately. Therefore I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.

During DTP 2008, I consulted a number of people and was suggested at least three solutions. I am going to summarise them in turn.

Canonical Examples

With each approach I would like to tackle two tasks. Given the following function dec:

dec : ℕ -> ⊤ ⊎ (ℕ × ℕ)
dec zero = inj₁ tt
dec (suc n) = inj₂ (n , n)

One may attempt to define a function down using unfoldr such that down n produces a list from n to 0. As mentioned above, unfoldr cannot pass the termination check. In fact, even the following definition fails the termination check:

down : ℕ -> [ ℕ ]
down n with dec n
... | inj₁ _ = []
... | inj₂ (a , n') with down n'
...    | x = a ∷ x

The first task is to define down using some kind of unfold.

In the second tasks, given a non-empty list, we would like to distribute its elements to a roughly balanced binary tree. The list and the tree are define by:

data List⁺ (a : Set) : Set where
    [_]⁺ : a -> List⁺ a
    _∷⁺_ : a -> List⁺ a -> List⁺ a
data Tree⁺ (a : Set) : Set where
    Tip⁺ : a -> Tree⁺ a
    Bin⁺ : Tree⁺ a -> Tree⁺ a -> Tree⁺ a

If we apply, for example, foldT merge wrap, we get merge sort (I use non-empty lists to save the constructor for empty trees). In Haskell, one might first define a function that splits a list to roughly two halfs, something equivalent to this:

split⁺ : {a : Set} -> List⁺ a -> a ⊎ (List⁺ a × List⁺ a)
split⁺ [ x ]⁺ = inj₁ x
split⁺ (x ∷⁺ xs) with split⁺ xs
... | inj₁ y = inj₂ ([ y ]⁺ , [ x ]⁺)
... | inj₂ (ys , zs) = inj₂ (zs , x ∷⁺ ys)

and use an unfold on Tree⁺. The second task is to construct a function expand : {a : Set} -> List⁺ a -> Tree⁺ a that builds a roughly balanced tree, using some kind of unfold that makes use of split⁺, or at least some variation of it.

Josh Ko’s Approach

Josh and I tried to extend unfolds with extra arguments representing a bound and proofs that the bound decreases with each call to f:

unfoldr↓ : {a b : Set} {_≾_ : b -> ℕ -> Set} ->
  (f : b -> ⊤ ⊎ (a × b)) -> (y : b) -> (t : ℕ) ->
  y ≾ t -> (forall {y} -> y ≾ zero -> f y ≡ inj₁ tt) ->
    (forall {y} t' {x y'} ->
         y ≾ suc t' -> f y ≡ inj₂ (x , y') -> y' ≾ t')
      -> [ a ]

Apart from the generating function f and the seed b, the function unfoldr↓ takes a bound t, a natural number. The seed and the bound is related by ≾, to be defined for each specific problem. Before producing the list, unfoldr↓ demands that the current seed is bounded by the bound (y ≾ t), a proof that f must yield inj₁ when the bound is zero, and a proof that if f returns inj₂ (x , y'), the new seed y' is bounded by a strictly smaller bound.

To define unfoldr↓ we need the inspect idiom (see the explanation in Relation.Binary.PropositionalEquality):

unfoldr↓ f y t y≾t p1 p2 with inspect (f y)
... | (inj₁ tt) with-≡ inj₁≡fy = []
... | (inj₂ (x , y')) with-≡ inj₂≡fy with t
...  | zero = contradiction (p1 y≾t)
        (\fy≡inj₁ -> inj₁≢inj₂ (≡-sym (≡-trans inj₂≡fy fy≡inj₁)))
...  | suc t' = x ∷ unfoldr↓ f y' t'
            (p2 t' y≾t (≡-sym inj₂≡fy)) p1 p2

Notice that unfoldr↓ passes the termination check because it pattern matches on t.

Descending List

For the first task, the seed is a natural number, and we may simply define ≾ to be ≤:

_≾_ : ℕ -> ℕ -> Set
n ≾ c = n ≤ c

Then down↓ can be defined in terms of unfoldr↓ and dec by:

stop : forall {n} -> n ≾ zero -> dec n ≡ inj₁ tt
stop {.zero} z≤n = ≡-refl

proceed : forall {n} c' {x n'} -> n ≾ suc c' -> dec n ≡ inj₂ (x , n') -> n' ≾ c'
proceed {.zero} c' {x} {n'} z≤n dec-zero≡inj₂ = contradiction dec-zero≡inj₂ inj₁≢inj₂
proceed {suc m} c' {.m} {.m} (s≤s m≤c') ≡-refl = m≤c'

down↓ : ℕ -> [ ℕ ]
down↓ n = unfoldr↓ dec n n ≤-refl stop proceed

where ≤-refl : forall x -> x ≤ x.

Expanding a Binary Tree

The unfold above can be generalised to trees in the obvious way:

unfoldT↓ : {a b : Set} {_≼_ : b -> ℕ -> Set} ->
  (f : b -> a ⊎ b × b) -> (y : b) -> (n : ℕ) ->
   y ≼ n -> (forall y -> y ≼ zero -> ∃ a (\x -> f y ≡ inj₁ x)) ->
    (forall y i y₁ y₂ ->
        y ≼ suc i -> f y ≡ inj₂ (y₁ , y₂) -> (y₁ ≼ i × y₂ ≼ i))
    -> Tree⁺ a
unfoldT↓ f y n y≼n p₁ p₂ with inspect (f y)
... | inj₁ x with-≡ _ = Tip⁺ x
... | inj₂ (y₁ , y₂) with-≡ inj₂≡fy with n
...  | zero = contradiction (proof (p₁ y y≼n))
      (\fy≡inj₁ -> inj₁≢inj₂ (≡-sym (≡-trans inj₂≡fy fy≡inj₁)))
...  | suc m with p₂ y m y₁ y₂ y≼n (≡-sym inj₂≡fy)
...    | (y₁≼m , y₂≼m) = Bin⁺ (unfoldT↓ f y₁ m y₁≼m p₁ p₂)
      (unfoldT↓ f y₂ m y₂≼m p₁ p₂)

One would wonder whether the condition (y₁ ≼ i × y₂ ≼ i) is too restrictive. When the proposition has to be proved inductively, we may need a stronger inductive hypothesis, for example, that both y₁ and y₂ are bounded by half of suc i. The current definition luckily works for our second task. We may need some generalisation later.

Repeated calls to split⁺ eventually terminates because the lengths of the lists are strictly decreasing. Therefore we define:

_#≤_ : {A : Set} -> List⁺ A -> ℕ -> Set
xs #≤ n = pred (length⁺ xs) ≤ n

With properly defined lemma1 and lemma2, we can expand the tree by unfoldT↓:

expand↓ : {a : Set} -> List⁺ a -> Tree⁺ a
expand↓ {a} xs = unfoldT↓ {a} {List⁺ a} {_#≤_} split⁺ xs
      (pred (length⁺ xs)) ≤-refl lemma1 lemma2

where the two lemmas respectively have types:

lemma1 : {a : Set}(xs : List⁺ a) ->
   xs #≤ zero -> ∃ a (\x -> split⁺ xs ≡ inj₁ x)
lemma2 : {a : Set} (xs : List⁺ a) (i : ℕ)
  (ys : List⁺ a) (zs : List⁺ a) ->
  xs #≤ suc i -> split⁺ xs ≡ inj₂ (ys , zs) -> ys #≤ i × zs #≤ i

Definition of lemma1 is a simple application of contradiction. On the other hand, lemma2 is very tedious to define. It appears to me that the definition inevitably becomes cumbersome because split⁺ and lemma2 are defined separately. It could be much easier if split⁺ is defined to return the computed results as well as some proofs about them. For my application in AoPA, however, I would prefer to be able to reuse the old split⁺. I don’t know a good solution yet.

Nils Anders Danielsson suggested that it would be nicer to integrate the bound into the type of the seed, while Conor McBride suggested yet another approach. I will try to summarise them next time.

To be continued…