We can eliminate the repeated list concatenations of levelt and
levelf by using accumulating parameters.  The specifications are:

    levelt' ∷ Rose α → List (List α) → List (List α)
    levelt' t = lzw appendL (levelt t)

    levelf' ∷ Forest α → List (List α) → List (List α)
    levelf' ts = lzw appendL (levelf ts)


## Exercise 3.35

Derive the definitions of ‘levelt'’ and ‘levelf'’.

The point-free versions of the specs. above come in handy:

    levelt' = lzw appendL ∘ levelt
    levelf' = lzw appendL ∘ levelf

For convenience:

    (levelt, levelf) = (foldR f g, foldF f g)
      where
        f x xss = Cons (wrap x) xss
        g       = foldL (lzw appendL) Nil

(a) levelt'

We have the specification

    levelt' t xss = lzw appendL (levelt t) xss

We consider the tree t and the accumulating parameter xss.

Case t = (Node a Nil), xss = Nil:

      lzw appendL (levelt (Node a Nil)) Nil

    =   { lzw.2 }

      levelt (Node a Nil)

    =   { levelt.1, foldR.1 }

      f a (foldF f g Nil)
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { foldF.1, mapL.1 }

      f a (g Nil)
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { g def., foldL.1 }

      f a Nil
        where
          f x xss = Cons (wrap x) xss

    =   { f def. }

      Cons (wrap a) Nil

which gives us a solution for this case.

We can extract a part of the above as a useful shortcut-lemma:

Lemma 1:

    levelt (Node a Nil) = Cons (wrap a) Nil

Proof: See above.

Case (Cons xs xss):

      lzw appendL (levelt (Node a Nil)) (Cons xs xss)

    =   { lemma 1 }

      lzw appendL (Cons (wrap a) Nil) (Cons xs xss)

    =   { lzw.4 }

      Cons (appendL (wrap a) xs) (lzw appendL xss Nil)

    =   { lzw.2 }

      Cons (appendL (wrap a) xs) xss

    =   { wrap.1, appendL.1 & 2 }

      Cons (Cons a xs) xss

which gives a solution for the case.

Case (Node a ts), ts ≠ Nil, xss = Nil:

      lzw appendL (levelt (Node a ts)) Nil

    =   { levelt.1 }

      lzw appendL (foldR f g (Node a ts)) Nil
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { foldR.1, f def. }

      lzw appendL (Cons (wrap a) (foldF f g ts)) Nil
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { lzw.2 }

      Cons (wrap a) (foldF f g ts)
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { lzw.2, levelf.1 }

      Cons (wrap a) (lzw appendL (levelf ts) Nil)

    =   { rewrite as composition, specification }

      Cons (wrap a) (levelf' ts Nil)

which gives us a solution for this case.

We can unify this with the first equation by observing that

    levelf' Nil Nil = Nil,

and so Cons (wrap a) Nil = Cons (wrap a) (levelf' Nil Nil).

Quick proof:

    levelf' ts Nil
      = lzw appendL (levelf Nil) Nil
      = lzw appendL (foldF f g Nil) Nil
          where g = foldL (lzw appendL) Nil
      = lzw appendL (g (mapL (foldR f g) Nil)) Nil
      = lzw appendL (g Nil) Nil
      = lzw appendL Nil Nil
      = Nil

So we have, thus far,

    levelt' (Node a ts) Nil            = Cons (wrap a) (levelf' ts Nil)
    levelt' (Node a Nil) (Cons xs xss) = Cons (Cons a xs) xss

Case (Node a ts), ts ≠ Nil, (Cons xs xss):

      lzw appendL (levelt (Node a ts)) (Cons xs xss)

    =   { levelt.1 }

      lzw appendL (foldR f g (Node a ts)) (Cons xs xss)
        where
          f y yss = Cons (wrap y) yss
          g       = foldL (lzw appendL) Nil

    =   { foldR.1, f def. }

      lzw appendL (Cons (wrap a) (foldF f g ts)) (Cons xs xss)
        where
          f y yss = Cons (wrap y) yss
          g       = foldL (lzw appendL) Nil

    =   { lzw.4 }

      Cons (appendL (wrap a) xs) (lzw appendL (foldF f g ts) xss)
        where
          f y yss = Cons (wrap y) yss
          g       = foldL (lzw appendL) Nil

    =   { rewrite as composition, specification }

      Cons (appendL (wrap a) xs) (levelf' ts xss)

    =   { wrap.1, appendL.1 & 2 }

      Cons (Cons a xs) (levelf' ts xss)

We can replace the previously-derived equation

    levelt' (Node a Nil) (Cons xs xss) = Cons (Cons a xs) xss

with what we’ve derived above by generalizing Nil to ts, provided we
can show that

    levelf' Nil xss = xss

for finite lists xss.

Quick proof:

    levelf' Nil xss
      = lzw appendL (levelf Nil) xss

      = lzw appendL (foldF f g Nil) xss
          where
            f x xss = Cons (wrap x) xss
            g       = foldL (lzw appendL) Nil

      = lzw appendL (g (mapL (foldR f g) Nil)) xss

      = lzw appendL (foldL (lzw appendL) Nil Nil) xss

      = lzw appendL Nil xss

      = xss
∎

So we have

    levelt' (Node a ts) Nil            = Cons (wrap a) (levelf' ts Nil)
    levelt' (Node a ts) (Cons xs xss)  = Cons (Cons a xs) (levelf' ts xss)

This semi-completes the synthesis of levelt'; to complete it, we must
still calculate a definition for levelf'.


(b) levelf'

We have the specification

    levelf' ∷ Forest α → List (List α) → List (List α)
    levelf' = lzw appendL ∘ levelf

We calculate by case analysis on the input Forest and accum-list.

Case Nil, xss: Immediate from the above quicky proof:

    levelf' Nil xss = xss

Case (Cons t ts), xss:

      lzw appendL (levelf (Cons t ts)) xss

    =   { levelf.1 }

      lzw appendL (foldF f g (Cons t ts)) xss
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { foldF.1 }

      lzw appendL (g (mapL (foldR f g) (Cons t ts))) xss
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { g def. }

      lzw appendL (foldL (lzw appendL) Nil (mapL (foldR f g) (Cons t ts))) xss
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { foldL-mapL fusion }

      lzw appendL (foldL (lzw appendL ∘ foldR f g) Nil (Cons t ts)) xss
        where
          f x xss = Cons (wrap x) xss
          g       = foldL (lzw appendL) Nil

    =   { levelt.1 }

      lzw appendL (foldL (lzw appendL ∘ levelt) Nil (Cons t ts)) xss

    =   { specification }

      lzw appendL (foldL levelt' Nil (Cons t ts)) xss

How can we proceed?  We have the types

    xss                                             ∷ List (List α)
    foldL levelt' Nil (Cons t ts)                   ∷ List (List α)
    lzw appendL (foldL levelt' Nil (Cons t ts)) xss ∷ List α

We should be able to eliminate the lzw appendL, as we did in the
definition of levelf'.  Let’s try to move forward by a case analysis
on xss.

Case xss = Nil:

      lzw appendL (foldL levelt' Nil (Cons t ts)) Nil

    =   { foldL.2 }

      lzw appendL (levelt' t (foldL levelt' Nil ts)) Nil

Since we know that (levelt' t xs) is non-empty for all finite xs, we
can just applying lzw.2 and jump to:

    foldL levelt' Nil (Cons t ts)

So far, we have

    levelf' Nil xss         = xss
    levelf' (Cons t ts) Nil = foldL levelt' Nil (Cons t ts)

Using foldL.1 (foldL f xss Nil = xss), we can generalize the second
equation to encompass the first.

    levelf' ts xss = foldL levelt' xss ts

Actually, this gives us a complete definition!  We don’t need to get
any further into the weeds with the case xss ≠ Nil.

While we eventually solved this exercise, the derivations were pretty
hairy and involved a lot of blundering around to derive redundant
results.  Can we calculate these functions more elegantly?