exercise_3.29.md

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