## Exercise 3.37

Use Hughes’s representation of lists as list transformers to derive
alternative versions of levelt' and levelf':

    levelt" ∷ Rose α → List (List α → List α)
    levelf" ∷ Forest α → List (List α → List α)

We can use the abstraction and representation functions defined by
Hughes:

    abst ∷ (List α → List α) → List α
    abst x = x Nil

    rep ∷ List α → (List α → List α)
    rep = appendL

Then, I suppose, we can write some specifications.

    levelt" = mapL rep ∘ levelt
    levelf" = mapL rep ∘ levelf

To calculate levelt", we can use foldR fusion.  We have

    mapL rep ∘ foldR f g = foldR f' g'

if

    g' ∘ mapL (mapL rep) = mapL rep ∘ foldL (lzw appendL) Nil

and

    (f' xs) ∘ mapL rep = mapL rep ∘ Cons (wrap xs),
      for all xs

Let's try to calculate a definition for f'.  We have the type

      f' xs (mapL rep yss) = mapL rep (Cons (wrap xs) yss)

    ≡  { mapL.2 }

      f' xs (mapL rep yss) = Cons (rep (wrap xs)) (mapL rep yss)

    ≡  { generalize (mapL rep yss) to gs }

      f' xs gs = Cons (rep (wrap xs)) gs

which gives us a definition for f'.

Now, g' ∷ List (List (Hughes α)) → List (Hughes α).  We use a case
analysis on the list xss.

Case Nil:

      g' (mapL (mapL rep) Nil) = mapL rep (foldL (lzw appendL) Nil Nil)

    ≡  { mapL.1 twice, foldL.1 }

      g' Nil = Nil

Case (Cons xs xss):

      g' (mapL (mapL rep) (Cons xs xss)) =
        mapL rep (foldL (lzw appendL) Nil (Cons xs xss))

    ≡  { foldL.2 }

      g' (mapL (mapL rep) (Cons xs xss)) =
        mapL rep (lzw appendL xs (foldL (lzw appendL) Nil xss))

    ≡  { theorem: mapL rep (lzw appendL xs ys) =
           lzw appendR (mapL rep xs) (mapL rep ys) }

      g' (mapL (mapL rep) (Cons xs xss)) =
        lzw appendR (mapL rep xs) (mapL rep (foldL (lzw appendL) Nil xss))

    ≡  { hypothesis }

      g' (mapL (mapL rep) (Cons xs xss)) =
        lzw appendR (mapL rep xs) (g' (mapL (mapL rep) xss))

    ≡  { mapL.2 }

      g' (Cons (mapL rep xs) (mapL (mapL rep) xss)) =
        lzw appendR (mapL rep xs) (g' (mapL (mapL rep) xss))

    ≡  { generalize (mapL rep xs) to ks and (mapL (mapL rep) xss) to kss }

      g' (Cons ks kss) = lzw appendR ks (g' kss)

Using the universal property of foldL, it’s easy to see that g' is a
fold:

    g' kss = case kss of
               Nil → Nil
               Cons ks kss → (lzw appendR) ks (g' kss)

So we have

    g' = foldL (lzw appendR) Nil

Putting the definitions of f' and g' together, we have a definition
for levelt" and levelf".

    (levelt", levelf") = (foldR f' g', foldF f' g')
      where
        f' xs = Cons (rep (wrap xs))
        g'    = foldL (lzw appendR) Nil