## Exercise 3.30

We can get something that looks like a universal property for each
of foldR and foldF by subbing-in the definition of the other function.
For h ∷ Rose α → β, we have

    h = foldR f g

    iff

    h (Node a ts) = f a (foldF f g ts)

And for h ∷ Forest α → γ:

    h = foldF f g

    iff

    h ts = g (mapL (foldR f g) ts)

Unfortunately, expanding this last equation using the equations for
mapL (by case analysis on ts) doesn’t clarify things much.  So here
it stands.

### Fusion

Here are the equations we are interested in solving:

    h ∘ foldR f g = foldR f′ g′, for all h ∷ β → δ

    h ∘ foldF f g = foldF f′ g′, for all h ∷ γ → δ

We can use the universal property of foldR.

    h ∘ foldR f g = foldR f′ g′

    iff

    (h (foldR f g (Node x ts))) = f′ x (foldF f′ g′ ts)

Let’s look at the foldF fusion law first.  Using the universal property,
we have

    h ∘ foldF f g = foldF f′ g′

    iff

    h (foldF f g ts) = g′ (mapL (foldR f′ g′) ts)

We can derive a constraint for the g′ function:

      h (foldF f g ts) = g′ (mapL (foldR f′ g′) ts)

    ≡   { foldF.1 }

      h (g (mapL (foldR f g) ts)) = g′ (mapL (foldR f′ g′) ts)

    ≡   { universal property of foldR }

      h (g (mapL (foldR f g) ts)) = g′ (mapL (h ∘ foldR f g) ts)

    ≡   { mapL fusion }

      h (g (mapL (foldR f g) ts)) = g′ (mapL h (mapL (foldR f g) ts))

    ≡   { generalizing (mapL (foldR f g) ts) to ys }

      h (g ys) = g′ (mapL h ys)

    ≡   { rewrite as composition }

      h ∘ g = g′ ∘ mapL h

Can we use this equation to derive a constraint for f′?  Let’s assume
that it holds for h, g, and g′ in the following.  We return to the
equation that we got from applying the universal property, and reason
as follows:

      f′ x (foldF f′ g′ ts) = h (foldR f g (Node x ts))

    ≡   { foldR.1 }

      f′ x (foldF f′ g′ ts) = h (f x (foldF f g ts))

    ≡   { foldF.1, twice }

      f′ x (g′ (mapL (foldR f′ g′) ts)) = h (f x (g (mapL (foldR f g) ts)))

    ≡   { universal property of foldR }

      f′ x (g′ (mapL (h ∘ foldR f g) ts)) = h (f x (g (mapL (foldR f g) ts)))

    ≡   { mapL fusion }

      f′ x (g′ (mapL h (mapL (foldR f g) ts))) = h (f x (g (mapL (foldR f g) ts)))

    ≡   { g′ ∘ mapL h = h ∘ g }

      f′ x (h (g (mapL (foldR f g) ts))) = h (f x (g (mapL (foldR f g) ts)))

    ≡   { generalizing (mapL (foldR f g) ts) to ys }

      f′ x (h (g ys)) = h (f x (g ys))

    ≡   { rewrite as point-free composition }

      (f′ x) ∘ h ∘ g = h ∘ (f x) ∘ g

    ≡   { generalizing to eliminate g }

      (f′ x) ∘ h = h ∘ (f x)

which gives us another constraint.

So far, we′ve established that

    h ∘ foldF f g = foldF f′ g′ ⇐ g′ ∘ mapL h = h ∘ g

    h ∘ foldR f g = foldR f′ g′ ⇐
        (g′ ∘ mapL h = h ∘ g) ∧ (∀x (f′ x) ∘ h = h ∘ (f x))

Does the second requirement for foldR also hold for f, g, h, and f′ in
foldF?  Given both constraints, can we derive

    h ∘ foldF f g = foldF f′ g′

It seems that we should be able to, since they give us an “induction
hypothesis” in the form of the fusion law for foldR.

So let’s assume

    g′ ∘ mapL h = h ∘ g            (I)
    ∀x (f′ x) ∘ h = h ∘ (f x)      (II)

We reason as follows: For finite Forests ts,

      h (foldF f g ts)

    ≡   { foldF.1 }

      h (g (mapL (foldR f g) ts))

    ≡   { unapply h and g, (I), apply g′ ∘ mapL h }

      g′ (mapL h (mapL (foldR f g) ts))

    ≡   { mapL fusion }

      g′ (mapL (h ∘ foldR f g) ts)

    ≡   { (I) + (II) + foldR fusion }

      g′ (mapL (foldR f′ g′) ts)

    ≡   { foldF.1 }

      foldF f′ g′ ts

as required. ∎  So (II) is actually only required to apply foldR fusion,
and is otherwise unused.