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...**