# Exercise 3.13
‘insert’, (way) above can be defined as an unfold. Do it.
insert ∷ Ord α ⇒ α → List α → List α
insert y Nil = wrap y
insert y (Cons x xs)
| y < x = Cons y (Cons x xs)
| otherwise = Cons x (insert y xs)
The hint is that the first (List α) element of the “state” tuple is
the list into which to insert the maybe-wrapped second element. Once
the element has been inserted, later unfold steps get Nothing.
As the exercises suggests, it’s a lot easier to do this with unfoldL′.
The hint gives us
insert y = unfoldL′ f u
where
f ∷ ((List α, Maybe α) → Maybe (α, (List α, Maybe α)))
u ∷ (List α, Maybe α)
We have:
insert' y xs = unfoldL′ ins (xs, Just y)
ins (Nil, Nothing) = Nothing
ins (Nil, Just x) = Just (x, (Nil, Nothing))
ins (Cons z zs, Nothing) = Just (z, (zs, Nothing))
ins (Cons z zs, Just x)
| x < z = Just (x, (Cons z zs, Nothing))
| otherwise = Just (z, (zs, Just x))
This definition is a bit unwieldy! In particular, it seems a little
inelegant to not be able to generate the tail (wrap x) in the second
equation for ins. (Scheme's unfold, with its tail-gen procedure, can
do this.)
But I’m pretty sure it’s correct. We need to prove this.
insert y xs = insert' y xs
The proof of the above proposition is by induction on the list xs.
Case Nil:
insert' y Nil
= { insert'.1 }
unfoldL' ins (Nil, Just y)
= { ins.2, unfoldL'.1 }
case Just (y, (Nil, Nothing)) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL′ ins v)
= { case, pattern matching }
Cons y (unfoldL′ ins (Nil, Nothing))
= { unfoldL'.1 }
Cons y (case ins (Nil, Nothing) of
Nothing → Nil
Just (x, v) → …)
= { ins.1 }
Cons y (case Nothing of
Nothing → Nil
Just (x, v) → …)
= { case, pattern matching }
Cons y Nil
= { wrap.1 }
wrap y
= { insert.1 }
insert y Nil
which establishes the case.
For the inductive step, we need the following lemma.
Lemma: unfoldL' ins (xs, Nothing) = xs
The proof is by structural induction on the list xs.
Case Nil:
unfoldL' ins (Nil, Nothing)
= { unfoldL'.1 }
case ins (Nil, Nothing) of
Nothing → Nil
Just (x, v) → …
= { ins.1 }
case Nothing of
Nothing → Nil
Just (x, v) → …
= { case }
Nil
which establishes the case.
Case Cons y ys:
unfoldL' ins (Cons y ys, Nothing)
= { unfoldL'.1 }
case ins (Cons y ys, Nothing) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
= { ins.3 }
case Just (z, (zs, Nothing)) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
= { case, pattern matching }
Cons z (unfoldL' ins (zs, Nothing))
= { hypothesis }
Cons z zs
which establishes the case. ∎
Case Cons z zs:
insert' y (Cons z zs)
= { insert'.1 }
unfoldL' ins (Cons z zs, Just y)
= { unfoldL'.1 }
case ins (Cons z zs, Just y) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
We have two subcases to consider.
Subcase y < z:
= { ins.4 }
case Just (y, (Cons z zs, Nothing)) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
= { case, pattern matching }
Cons y (unfoldL' ins (Cons z zs, Nothing))
= { lemma }
Cons y (Cons z zs)
= { insert.2 }
insert y (Cons z zs)
Subcase y ≥ z:
case ins (Cons z zs, Just y) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
= { ins.5 }
case Just (z, (zs, Just y)) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL' ins v)
= { case, pattern matching }
Cons z (unfoldL' ins (zs, Just y))
= { insert'.1 }
Cons z (insert' y zs)
= { hypothesis }
Cons z (insert y zs)
= { insert.2 }
insert y (Cons z zs)
which establishes the case. ∎
(Writing this proof revealed some mistakes in the def. of insert'!)