## 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. ∎