## Exercise 3.32

Write ‘lzw’ as an unfold.

First, it’s worth noting that zipWith is very easy to define as an
unfold:

    zw f = unfoldL p g h
      where
        p (xs, ys) = null xs || null ys
        g          = uncurry f ∘ both head
        h          = both tail

    zipWith f = curry (zw f)

with ‘both’ being the function-product combinator:

    both ∷ (α → β) → (α, α) → (β, β)
    both f (x, y) = (f x, f y)

With lzw, though, things are different.  We will work with an uncurried
version, lzw′.

Using the universal property of unfoldL, we have:

    lzw′ f = unfoldL p g h

    iff

    lzw′ f x = if p x then Nil else Cons (g x) (zw f (h x))

We have the following types:

    p ∷ (List α, List α) -> Bool
    g ∷ (List α, List α) -> α
    h ∷ (List α, List α) -> (List α, List α)

A difficulty arises immediately: Nil is only the value of
(lzw′ f (xs, ys)) when xs and ys are both Nil--a case we will never
reach if the lists are of unequal length.

    p (xs, ys) = null xs && null ys

This looks less than promising.  If (p x) is false, we reason:

      lzw′ f z = if p z then Nil else Cons (g z) (zw f (h z))

    ≡   { ITE }

      lzw′ f z = Cons (g z) (zw f (h z))

Now we should have a case analysis, using the equations for lzw′.
Again, it seems like we have a problem: only lzw.3 has a right-hand
side of the form Cons y ys.  But we may be able to remedy this by
rewriting the first two equations so that the patterns are disjoint:

    lzw' f (Nil, Nil)       = Nil                                  (lzw'.1)
    lzw′ f (Nil, Cons y ys) = Cons y ys                             (lzw'.2)
    lzw′ f (Cons x xs, Nil) = Cons x xs                             (lzw'.3)
    lzw′ f (Cons x xs, Cons y ys) = Cons (f x y) (lzw' f (xs, ys))  (lzw'.4)

Now we try again to calculate.

Case z = (Nil, Cons y ys):

      Cons (g (Nil, Cons y ys)) (zw f (h (Nil, Cons y ys))) =
        lzw′ f (Nil, Cons y ys)

    ≡   { lzw′.1 }

      Cons (g (Nil, Cons y ys)) (zw f (h (Nil, Cons y ys))) =
        Cons y ys

    ≡   { define: g (Nil, Cons y ys) = y }

      Cons y (zw f (h (Nil, Cons y ys))) = Cons y ys

We appear to be stuck, since we can’t eliminate the (zw ...) term on
the left-hand side.

We can fare much better if we instead define lzw as an apomorphism.
(But see below, after this exercise.)

We seek a definition of the form

    lzw' f = apoL' g

We proceed by case analysis on the tuple argument p.  The first case
is easy.

Case p = (Nil, Nil):

      apoL' g (Nil, Nil) = lzw' f (Nil, Nil)

    ≡   { apoL'.1, lwz'.1 }

      (case g (Nil, Nil) of
        Nothing -> Nil
        ...)                 = Nil

So we define

    g (Nil, nil) = Nothing

Case p = (Cons x xs, Nil):

      apoL' g (Cons x xs, Nil) = lzw' f (Cons x xs, Nil)

    ≡   { apoL'.1, lzw'.2 }

      (case g (Cons x xs, Nil) of
        Nothing -> Nil
        Just (z, Left v) -> Cons z (apoL' g v)
        Just (z, Right zs) -> Cons z zs)       = Cons x xs

We define:

    g (Cons x xs, Nil) = Cons x xs

The case p = (Nil, Cons y ys) is almost identical, and gives us

    g (Nil, Cons y ys) = Cons y ys

Case p = (Cons x xs, Cons y ys).  We assume as an induction hypothesis
that lzw' f (xs, ys) = apoL' g (xs, ys).

      apoL' g (Cons x xs, Cons y ys) = lzw' f (Cons x xs, Cons y ys)

    ≡   { apoL'.1, lzw'.4 }

      (case g (Cons x xs, Cons y ys) of
        Nothing -> Nil
        Just (z, Left v) -> Cons z (apoL' g v)
        Just (z, Right zs) -> Cons z zs)       = Cons (f x y)
                                                   (lzw' f (xs, ys))

    ≡   { hypothesis }

      (case g (Cons x xs, Cons y ys) of
        Nothing -> Nil
        Just (z, Left v) -> Cons z (apoL' g v)
        Just (z, Right zs) -> Cons z zs)       = Cons (f x y) (apoL' g (xs, ys))

We define:

    g (Cons x xs, Cons y ys) = Just (f x y, Left (xs, ys))

Putting together our definition, we have:

    lzw' f = apoL' g
      where
        g (Nil, Nil)             = Nothing
        g (Cons x xs, Nil)       = Cons x xs
        g (Nil, Cons y ys)       = Cons y ys
        g (Cons x xs, Cons y ys) = Just (f x y, Left (xs, ys))

And, of course,

    lzw f = curry (lzw f)

*  *  *

Actually, defining the apomorphism version of lzw is the subject of
exercise 3.33!  So there must be a way to define lzw as an unfold.

And here it is.  Gibbons gives us a hint--it’s inefficient because the
longer of the two lists must be reconstructed.

    lzwu f = unfoldL' g
      where
        g (Nil, Nil)             = Nothing
        g (Cons x xs, Nil)       = Just (x, (xs, Nil))
        g (Nil, Cons y ys)       = Just (y, (Nil, ys))
        g (Cons x xs, Cons y ys) = Just (f x y, (xs, ys))

We will prove that this definition is equivalent to the directly
recursive definition by induction on the input list-pair.

Case (Nil, Nil):

      lzwu f (Nil, Nil)

    =   { lzwu.1 }

      unfoldL' g (Nil, Nil)

    =   { unfoldL'.1 }

      case g (Nil, Nil) of
        Nothing -> Nil
        -- ...

    =   { lzwu.g.1, pattern matching, case }

      Nil

    =   { lzw'.1 }

      lzw' f (Nil, Nil)

which establishes the case.

Case (Cons x xs, Nil).  We use the following induction hypothesis:

    lzwu f (xs, Nil) = lzw' f (xs, Nil),

reasoning as follows:

      lzwu f (Cons x xs, Nil)
    = unfoldL' g (Cons x xs, Nil)

    =   { unfoldL'.1 }

      case g (Cons x xs, Nil) of
        Nothing     → Nil
        Just (y, v) → Cons y (unfoldL′ g v)

    =   { lzwu.g.2, case, pattern-matching }

      Cons x (unfoldL' f (xs, Nil))

    =   { hypothesis }

      Cons x (lzw' f (xs, Nil))

    =   { lzw'.1 }

      Cons x xs

    =   { lzw'.1 }

      lzw' f (Cons x xs, Nil)

which establishes the case.

The case (Nil, Cons y ys) is almost identical.

Case (Cons x xs, Cons y ys).  Again we use the usual hypothesis.

      lzwu f (Cons x xs, Cons y ys)
    = unfoldL' g (Cons x xs, Cons y ys)

    =   { unfoldL'.1 }

      case g (Cons x xs, Cons y ys) of
        Nothing     → Nil
        Just (z, v) → Cons z (unfoldL′ g v)

    =   { lzwu.g.4, case, pattern-matching }

      Cons (f x y) (unfoldL' g (xs, ys))

    =   { lzwu.1, hypothesis }

      Cons (f x y) (lzw' f (xs, ys))

    =   { lzw'.3 }

      lzw' f (Cons x xs, Cons y ys)

which establishes the case. ∎