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]

I disagree because, if we set r = p, we will get the type `p → a → p → p`, but we cannot rewrite this type as `p → f p` where `f p` is covariant in p.

The type `p → a → p → p` is equivalent to `p × a × p → p` or `p → a × p → p`, etc., but there will be always a trailing ` → p` in that type. You cannot rewrite `p → a → p → p` as `p → f p` where `f` is a polynomial endofunctor or any covariant endofunctor.

Another thing occurred to me. Looking again at the type signature `SassaHylo : c a → (c a → f a r → r) → r` I notice a similarity to paramorphisms.

https://stackoverflow.com/questions/13317242/what-are-paramorphisms

cata :: Functor f => (f t -> t) -> Fix f -> t
para :: Functor f => (f (Fix f, t) -> t) -> Fix f -> t

To see the similarity, we need to replace our bifunctor f by a simple functor and note that `Fix f` is the analog of `c a` in my notation. Flip the curried arguments, denote c = Fix f, and find:

para :: Fix f -> (f (Fix f, t) -> t) -> -> t

para :: c → ∀ t. (f (c × t) → t) → t

SassaHylo : c → ∀ r. (c × f r → r) → r

Replacing the Church encoding by the µ operation as µ t. g t = ∀ t. (g t → t) → t (where `g` is any covariant endofunctor), we find:

para :: c → µ t. f (c × t)

SassaHylo : c → µ t. c × f t

The remaining difference is between the types f (c × t) and c × f t under µ t.

But those two types are related: if we write informally the infinitely nested types as:

µ t. f (c × t) = f (c × f (c × ...))

µ t. c × f t = c × f (c × f(c × ...))

We see that µ t. c × f t = c × µ t. f (c × t)

(This can be proved formally, of course.)

Denote d = µ t. f (c × t). The paramorphism's standard type is then just c → d, and SassaHylo's type is c → c × d.

Most likely, SassaHylo is just the paramorphism with an extra `c` tacked on top.

But this remains to be verified. I haven't yet checked (and it is not obvious) that your code for SassaHylo corresponds to my code for the function of type c → c × d.

[sassa_nf]

> notice a similarity to paramorphisms.

Very possible.

If I recall correctly, many *-morphisms can be expressed through each other.

[chaource]

Actually, could you simplify your code for zipping trees? I see a lot of `Bool` arguments that are not being used in any way. So far I am not able to adapt that code to an arbitrary Church encoding.

[sassa_nf]

The Bool argument is there to compute different values of p for left and right subtrees. The argument exists because of how I factored out the logic of computing these values from the logic of applying them. In a hylo these are factored differently: phi constructs (f a p), so it knows both how to compute different values of p, and where to plug them in what constructor.

I don't know how to modify that code to return (f a p) without adding a polynomial functor (Tr a x), ie how to use fix-point type (f a r -> r) -> r to represent (f a p) specifically.

If I do add Tr a x, I end up with the code in this post.

[chaource]

So far, I am not able to generalize the code from your previous post to arbitrary Church-encoded types. That code is quite complicated and specially tailored to the two specific data structures (list and tree). For instance, I was not able to rewrite the "tree hylo" to the same type as the "list hylo".

The code in the present post (Int -> hylomorphism with an explicit bound on recursion depth) seems more promising. The key to generalizing is to write the code of hylo and treezip as a function that is parametric in the recursion scheme `f`. Then the code will be automatically applicable for any Church-encoded type.

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