## Exercise 3.14
We’d like ‘insert’ to be able to make use of the remainder of the
input list; using unfold, this isn't possible, so the entire input
list must be traversed regardless of where the insertion occurs.
To fix this, we can define ‘insert’ as an *apomorphism* using the
following higher-order function:
apoL′ ∷ (β → Maybe (α, Either β (List α))) → β → List α
apoL′ f u = case f u of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
(BTW, it’s straightforward to define unfoldL′ as an apomorphism:
unfoldL′ f = apoL′ (g ∘ f)
where
g Nothing = Nothing
g Just (x, v) = Just (x, Left v)
Using the Maybe monad, we have g = fmap (mapSnd Left).
So, we have
insert″ y = apoL' f u
for some
f ∷ (β → Maybe (α, Either β (List α)))
u ∷ β
What is β here? For a first try, we just plug-in the ‘state’ type of
insert': (List α, Maybe α).
(Is there a method by which we could calculate a definition? Like
unfoldL and unfoldL', apoL' is tough to calculate with.)
insert″ y xs = apoL' ins' (xs, Just y)
ins' ∷ (List α, Maybe α) → Maybe (α, Either (List α, Maybe α) (List α))
ins' (Nil, Nothing) = Nothing
ins' (Nil, Just y) = Just (y, Right Nil)
ins' (Cons x xs, Nothing) = Just (x, Right xs)
ins' (Cons x xs, Just y)
| y < x = Just (y, Right (Cons x xs))
| otherwise = Just (x, Left (xs, Just y))
ins' is pretty awkward. There are a bunch of almost-overlapping cases
and a general sense of redundancy. Fortunately, we can simplify this
definition. The key realization is that the to-be-inserted value (or
its absence) no longer need to be part of the ‘state’; we can thus
parameterize ins' over this value.
ins' ∷ α -> List α → Maybe (α, Either (List α, Maybe α) (List α))
ins' y Nil = Just (y, Right Nil)
ins' y (Cons x xs)
| y < x = Just (y, Right (Cons x xs))
| otherwise = Just (x, Left xs)
insert″ y = apoL' (ins' y)
This is much nicer.
NTS: insert″ y xs = insert y xs, for finite lists xs.
The proof is by structural induction on xs.
Case Nil:
insert″ y Nil
= { insert″.1 }
apoL' (ins' y) Nil
= { apoL'.1 }
case ins' y Nil of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
= { ins'.1 }
case Just (y, Right Nil) of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
= { case, pattern matching }
Cons y Nil
= { wrap.1, insert.1 }
insert y Nil
which establishes the case.
Case (Cons z zs):
insert″ y (Cons z zs)
= { insert″.1 }
apoL' (ins' y) (Cons z zs)
= { apoL'.1 }
case ins' y (Cons z zs) of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
We have two subcases to consider.
Subcase y < z:
= { ins'.2 }
case Just (y, Right (Cons z zs)) of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
= { case, pattern matching }
Cons y (Cons z zs)
= { insert.2, y < z }
insert y (Cons z zs)
Subcase y ≥ z:
case ins' y (Cons z zs) of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
= { ins'.2 }
case Just (z, Left zs) of
Nothing → Nil
Just (x, Left v) → Cons x (apoL′ f v)
Just (x, Right xs) → Cons x xs
= { case, pattern matching }
Cons z (apoL' (ins' y) zs)
= { hypothesis }
Cons z (insert y zs)
= { insert.2, subcase def. }
insert y (Cons z zs)
which establishes the case. ∎