## Exercise 3.29

Show that the following is equivalent to foldR.

    foldRose ∷ (α → List β → β) → Rose α → β
    foldRose f (Node a ts) = f a (mapL (foldRose f) ts)

(a) We define foldRose in terms of foldR/foldF.

We can use the universal property from the next exercise to state:

    foldRose h = foldR f g

    iff

    foldRose h (Node x ts) = f x (foldF f g ts)

where t = Node a ts is any rose tree.

Using the definition of foldRose, this gives us the equation

      h x (mapL (foldRose h) ts) = f x (foldF f g ts)

    ≡   { foldR universal property }

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

    ≡   { foldF.1 }

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

    ≡   { generalizing (foldF f g ts) to xs, η-equivalence }

      h = f

Considering the type signature of foldR, we now have f ∷ α → List β → β,
so γ = List β and g ∷ List β → List β.  So let's consider the
following equation, which we can extract from the previous use of the
foldR universal property:

      foldF f g ts = mapL (foldRose f) ts

    ≡   { foldF.1 }

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

    ≡   { foldR universal property }

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

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

      g xs = xs

so we can define g = id.

This gives us the definition:

    foldRose f = foldR f id