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