Size-restricted recursion for hylomorphism

[sassa_nf]

...and here is a proper hylomorphism inspired by the last updates:

The main idea is: we can't have unrestricted recursion hylo p q = p . fmap (hylo p q) . q, but we can construct a recursive structure of a predefined size. So it is not a generic hylomorphism, but a hylomorphism for a problem of a known size. A constraint is: we need a "fixed point" value of the target type, which gets plugged on the last level of recursion, if we get to it.

(working code)

data Tr a x = TL | TN a x x

instance Functor (Tr a) where
  fmap f TL = TL
  fmap f (TN a l r) = TN a (f l) (f r)


newtype Nat = Nat {nat :: forall r. (r -> r) -> r -> r}

zero :: Nat
zero = Nat $ \_ -> id

suc :: Nat -> Nat
suc n = Nat $ \f -> f . nat n f

one = suc zero

two = suc one

three = suc two

add :: Nat -> Nat -> Nat
add x y = nat x suc y

mul :: Nat -> Nat -> Nat
mul x y = nat x (add y) zero

ex :: Nat -> Nat -> Nat
ex x y = nat y (mul x) one

five = add two three

thirtytwo = ex two five

-- turn 32-bit integers into church-encoded Nat - a size-bound "loop"
tonat :: Int -> Nat
tonat n = (\(x, _, _) -> x) $ nat thirtytwo pow (zero, one, n) where
  pow (n, m, x) = (add n (if even x then zero else m), add m m, x `div` 2)


hylo :: (Functor f) => Int -> (f b -> b) -> (a -> f a) -> b -> a -> b
hylo n psi phi z = (nat $ tonat n) (\f -> psi . fmap f . phi) (\_ -> z)

treezip :: Tree a -> Tree b -> Tree (a, b)
treezip xs ys = hylo (max (height xs) (height ys)) psi phi leaf (xs, ys) where
  phi (xs, ys) = option (val xs) TL
                 $ \x -> option (val ys) TL
                 $ \y -> TN (x, y) (left xs, left ys) (right xs, right ys)

  psi TL = leaf
  psi (TN v l r) = node v l r

Comments

[chaource]

Your `Tr` is the same as my `f`. It's the recursion scheme. It remains to rewrite everything in terms of `Tr` so that all functions are parameterized by `Tr`.

[sassa_nf]

Yes. The difference is that we don't attempt to make everything church-encoded. Like, hylo takes a co-algebra for f, but church-encoded fixed point of f does not have f. So Tr needs to be introduced. This is not the same as "if your type is a functor, hylo will work". It really is "create a polynomial functor for your church-encoded type, and then hylo will work".

[chaource]

We can perhaps relax our constraints: we do not necessarily need to Church-encode everything. What we want is to write code without recursion, where we are only allowed to use a given catamorphism for a given data type. The entire recursive and iterative functionality is encapsulated in the given catamorphism.

So, let us formulate the question like this:

We are given a type constructor `C`. We imagine that `C a` is a data structure containing some values of type `a`.

We know very little about `C` other than:

- We have a given bifunctor F. So, we have bimap: (a → p) → (b → q) → F a b → F p q

- We know that the type `C a` is isomorphic to the type `F a (C a)`. The isomorphism is witnessed by two functions:

fix: F a (C a) → C a

unfix: C a → F a (C a)

These functions are considered to be known.

- We have the catamorphism function:

cata: C a → ∀ r. (F a r → r) → r

- We have the Church encoding constructor:

church: (∀ r. (F a r → r) → r) → C a

These functions will satisfy a number of laws, but it's less important. For example: fix . unfix == id; unfix . fix == id; cata ca fix == ca; cata . church == id; church . cata == id; and so on.

And that's it. Now we want to implement various things though these functions. We are allowed to use any features of the (purely functional) language: product types, co-product types, functions, universal type quantifiers, whatever - but no recursion.

To implement some function for C a, we usually need to have a corresponding function for F a r. For example, we can implement fmap:

fmap: (a → b) → C a → C b

but only if we have bimap for F.

We can implement depth:

depth: C a → Int -- count the maximum recursion depth of a value.

but only if we have a "traverse" for F that works like this:

traverse: Applicative h => (r → h s) → F a r → h (F a s)

We can implement traverse for C a but only if we have bisequence for F (see my post here https://chaource.dreamwidth.org/229017.html ).

Using `depth`, we can transform any `C a` into a Church-encoded `Nat`, counting the maximum recursion depth. Then we can implement your `recursion-safe hylo` from this post.

So the "Church encoding approach" consists of asking: what functions can be implemented without recursion, if we are allowed to use catamorphisms and the properties of F.

Typically, F will be a simple, non-recursive polynomial bifunctor, like F a r = Maybe (a, r, r) for the type of trees that you considered. So we will have properties like bimap, traverse, bitraverse, etc., easily implementable for F without recursion.