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]

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.