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?