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

[juan_gandhi]

Wow, good idea, and the code is so beautiful! Thanks a lot!

[chaource]

This is interesting but I was thinking of something different: instead of an argument of type "natural" to bound the recursion, why not use a value of type "tree" (church-encoded ). We have in any case input values of that type.

[sassa_nf]

Yep. Look for a comment in the previous post. There I have ana that kicks off the recursion on a Tree.

The problem with that is that it works for trees where there is only one constructor with a hole. What if we have more than one? That won't generalize.

Other problems: which tree is bigger? Choosing a smaller tree is ok for a zip, but not a generic hylomorphism. What if anamorphism builds a Tree bigger than input?..


So I realized that in order to generalize need to use fmap, just restrict the recursion depth - ie make it provably finite. Note that I pick tree height, but I could just as well pick a 2^(2^256) or something equally ridiculous. So that it is finite as far as the compiler is concerned, but the resulting structure will never reach that size in practice. It may be fun to check that the lazy computation allows for such massive Nat.

[chaource]

Is there a problem with fmap? I thought fmap is always easy to define for church encodings.

[sassa_nf]

No problem with fmap. The problem is the self-reference:

Let me write that again for context:

hylo p q = p . fmap (hylo p q) . q


Also, since you are talking about fmap for church-encoded stuff, you may find it a surprise when you consider what fmap is needed for hylo.

[chaource]

In your first post, your version of Hylo was automatically size-restricted because its first argument was a List or a tree. Maybe you can rewrite Hylo so that it is always size-restricted?

The standard code for Hylo looks like this: given a functor f and an f- algebra "r " and an f- co-algebra "p", we construct a unique function p → r.

Standard Hylo: ( f r →r )→(p →f p) →p→r

Your non-standard version of Hylo instead takes a value of type of the initial f-algebra and then requires functions of type p → f r →r

Sassa Hylo: c → ( p → f p ) → (p → f r → r ) → p → r

Where c is the least fixpoint of f:

C = forall a. (f a→a ) →a

It remains to be seen whether the type of "sassa Hylo" is a correct generalization of your code to arbitrary types, and whether zip can be defined generally.

[sassa_nf]

In my previous post there were several hylos, including the one that uses input as the means of constraining the recursion. I've listed the problems with that. Basically, it is not general enough even for one type, let alone generalizing it for any recursive type.

Yep, I listed a standard hylo in the previous post, too, to demonstrate how it can find a fixed point of Tr a x. But it is defined through self-reference to hylo.

> Sassa Hylo: c → ( p → f p ) → (p → f r → r ) → p → r

No it's not. The post lists its actual type.

[chaource]

You gave type signatures only for lists and for a specific kind of a tree. I'm trying to generalize that to an arbitrary church- encoded types.

[sassa_nf]

eh?...

hylo :: (Functor f) => Int -> (f b -> b) -> (a -> f a) -> b -> a -> b

[chaource]

But this is not a generalization of the type signatures from your previous post.

[sassa_nf]

That's right, it is not. It is a complete rebuild of the solution, having revisited the 10+ yr old exercises.

Yet, you can probably see why that first solution is a sort of hylomorphism. It solves problems for specific types of (p -> f p) - such that they produce a value no bigger than the input tree, and such that use the value in the node, not the whole subtree. Also, the function is plugged in the wrong place, but it still has to know whether the seed value is for left or right, hence the Bool argument.

Taking these things into account, I tried to incorporate both trees into the type of the seed explicitly. Consequently, the output of the function becomes a tuple, or rather a Maybe tuple, since it should have a way to stop the recursion, which is represented by Tr a x here. The right design falls out of these considerations.

[chaource]

If we manage to rewrite your code (from the previous post ) for arbitrary church-encoded types, I believe it would be a discovery! The standard hylomophisms are not possible in church encoding due to non-termination.

[sassa_nf]

I treat the study in the previous post as a stepping stone to the results in this post. What do you like about it? What do you not like about the solution in this post?

What I don't like about the previous post - the list of items in the other comment.

What I like about this post:

hylo receives a proof of termination - or rather enforces termination, because we know what a finite recursive data structure ends with: a constructor for which fmap does not apply function and acts as id.

height is easy to write for arbitrary church-encoded types. Using this, we can write a zip for arbitrary church-encoded types.

Arbitrary coalgebras require a weak proof of termination: the size of the structure they are going to generate.

[chaource]

In the previous post, I like two aspects: that there is perhaps a new kind of Hylo with different type parameters, and that the termination witness is the input itself, rather than a separately computed number.

I don't like that the type signature of the new Hylo is complicated and not directly related to the algebra and the Coalgebra signatures. Because of that, it's far from clear that the new Hylo can ever work for all church-encoded types.

In this post, l like that the new Hylo is clearly generalizable to all church-encoded types.

I don't like two aspects: that the termination witness is a natural number that we have to compute separately, and that there is an extra "fallback" argument of type 'b‘ that we have to supply somehow.

The natural number is computed as the depth of some structure ( which we have to get somewhere) and then immediately used as a fold counter. Why not just fold over that structure? Ideally, I would want to reuse the input as a termination witness and at the same time as a "fallback" argument.

[sassa_nf]

> The natural number is computed as the depth of some structure ( which we have to get somewhere)

Yes, it is trivial to construct such a number for any given church-encoded types, so it is simply a generalization over construction of such values; ie you can use other ways to compute the depth; perhaps, without constructing the actual structure. Say, the size of Cartesian product can be calculated without constructing it.

> and then immediately used as a fold counter.

Yep, as part of a generalization.


> there is an extra "fallback" argument of type 'b‘ that we have to supply somehow.

Yes. However, this is trivial for finite inputs. As a proof of the input being finite, you should know what the ends of input look like. For polynomial functors F[A] it is one of constructors that doesn't contain a term of type A.

E.g for data Tr a x = TL | TN a x x such a constructor is TL - it doesn't contain any terms of type x. Note also that we could introduce a new constructor instead so that by the end of processing we would have a proof whether the computation ended before termination was forced. E.g internally we could use Either () b, and make hylo return that.

You can compute the value of type b as (psi TL), or, if it takes too much brain power, we could demand a value of type (f a) instead, and compute the value of type b for you.

[chaource]

I made some progress in understanding the "Sassa hylomorphisms", for lack of a better name.

Suppose `f` is a bifunctor and define `c a` as the Church-encoded least fixpoint of `f a`:

c a ≝ ∀r. (f a r → r) → r

This describes, for instance, Church-encoded lists: `c a ≅ List a` if we define `f` as:

f a r ≝ 1 + a × r ≝ Maybe (a, r)

Take the exact type signature of the "Sassa hylo" from your previous post:

Sassa hylo :: List a -> (p -> r) -> (p -> a -> p) -> (p -> a -> r -> r) -> (p -> r)

Note that `p` is not an f-coalgebra because we do not have an argument of type p → f p. That was my initial confusion. I was trying to make sense of `p` being an f-coalgebra, but this makes no sense especially since the Church encoding cannot be the terminal coalgebra.

Instead, I rewrite the type signature of `Sassa hylo` so that `f` is used as much as possible everywhere. Use the following type equivalences:

f a r → r ≅ (1 + a × r) → r ≅ (1 → r) × (a × r → r) ≅ r × (a → r → r)

Therefore:

(p → r) × (p → a → r → r) ≅ p → (r × (a → r → r)) ≅ p → f a r → r

Then rewrite the type signature of `Sassa hylo` as:

Sassa hylo : c a → (p → f a r → r) → (p → a → p) → p → r

Equivalently:

Sassa hylo : c a → (p → f a r → r) → (p → a → p) × p → r

Use another type equivalence:

(p → a → p) × p ≅ (p × a → p) × (1 → p) ≅ f a p → p

So, rewrite `Sassa hylo`'s type signature as:

Sassa hylo : c a → ∀r. ∀p. (p → f a r → r) → (f a p → p) → r

Flip arguments:

Sassa hylo : c a → ∀r. ∀p. (f a p → p) → (p → f a r → r) → r

This is already good enough: it works for arbitrary Church encodings. But how can we implement a function of that type?

Further simplify this type signature by using the "Church-Yoneda identity" (my terminology; proof omitted):

∀p. (f a p → p) → h p ≅ h (c a) -- here h may be any covariant endofunctor.

Use this identity with h p ≝ (p → f a r → r) → r and obtain:

Sassa hylo : c a → ∀r. (c a → f a r → r) → r

Note that ∀r. (c a → f a r → r) → r is the least fixpoint of the functor g r ≝ c a × f a r, that is, we can write:

∀r. (c a → f a r → r) → r ≝ µr. c a × f a r

This type seems to be larger than `c a`. But, `Sassa Hylo` is a function from `c a` into that type. All we need is to implement that function:

SassaHylo : c a → (c a → f a r → r) → r
SassaHylo ca cafarr = ca (cafarr ca)

Here `ca` has type `∀x. (f a x → x) → x` and is used with the type parameter x ≝ c a.

For easier usage, let us rewrite this implementation for the type signature that we had before using the Church-Yoneda identity:

SassaHylo : c a → (f a p → p) → (p → f a r → r) → r
SassaHylo ca fapp pfarr = ca (pfarr (ca fapp))

Here the `ca` in `ca fapp` is used with type parameter `p`, so that `ca fapp` has type `p` and can be used as the first argument for `pfarr`. But the `ca` in `ca (pfarr...)` is used with type parameter `r` and has type `r`.

It remains to be seen whether this implementation corresponds to the one given in your previous post, and whether it allows us to implement zip for an arbitrary Church encoding assuming suitable properties of `f`. For instance, we might require a function `zipf2 : f a r × f b s → f (a × b) (r × s)` for `zip` to work.

[sassa_nf]

Thank you for this very detailed account.

> Note that `p` is not an f-coalgebra because we do not have an argument of type p → f p

I think a lot is lost from not mentioning where forall r is.

For example

> p -> a -> p

can be seen as f a p -> p, which is an f-algebra.

> p -> a -> r -> r

Because this is forall r, pick r=p to get p -> f a p, which is an f-coalgebra.

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

[chaource]

I have traced the types in your code and found that your Hylo is quite different from the function I implemented above. (Although the type is the same.)

Your code is quite tricky but nevertheless can be
generalized to any church encoding. It is a fold where "c a" is applied to a function of type f a (p→r )→(p → r ), not to functions of type f a p→p.

Whether your code is equivalent to a paramorphism remains to be seen.

[sassa_nf]

Ok, I made a mistake, it is not p->f a p, it is p->f a (p->r)->r, so it is an algebra, although it tastes like co-algebra, because you get p->something. Because r can be (f a p), so you end up with f a (p->f a p)->p->f a p - you construct a co-algebra, given f a (...).

[chaource]

By the way - I found an interesting paper here: https://www.researchgate.net/publication/2813507_Deriving_Structural_Hylomorphisms_From_Recursive_Definitions
They show an algorithm for converting a large class of recursive functions into code that just calls some hylomorphisms.

This is interesting because, with a size-limited hylomorphism, we can finally ban runaway recursion, and yet write recursive code more or less freely.

[sassa_nf]

Thanks, that's interesting