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