# Exercise 3.4

Define insert₁ as a fold:

    insert₁      ∷ Ord α ⇒ α → List α → (List α, List α)
    insert₁ y xs = (xs, insert y xs)

Using the universal property of foldL, we have

    (insert₁ y) = foldL f e

iff

    (insert₁ y) xs = case xs of
                       Nil       → e
                       Cons z zs → f z ((insert₁ y) zs)

So we have the equations

    insert₁ y Nil         = e
    insert₁ y (Cons x xs) = f x (insert₁ y xs)

The first is easy.  By the definition above, we have

    insert₁ y Nil = (Nil, insert y Nil)
                  = (Nil, wrap y)

So given y : α, we have e = (Nil, wrap y).

In the second equation, we need to solve for
f ∷ α → (List α, List α) → (List α, List α).

      insert₁ y (Cons x xs) = f x (insert₁ y xs)

    ≡   { insert₁ def. }

      (Cons x xs, insert y (Cons x xs)) = f x (xs, insert y xs)

Consider the case y ≥ x.  We reason as follows:

      (Cons x xs, insert y (Cons x xs)) = f x (xs, insert y xs)

    ≡   { insert.2 }

      (Cons x xs, Cons x (insert y xs)) = f x (xs, insert y xs)

    ≡   { generalizing (insert y xs) to ys }

      (Cons x xs, Cons x ys) = f x (xs, ys)

So far, we have

    f x (xs, ys) = if y < x then ... else (Cons x xs, Cons x ys)

(where y is in the enclosing function’s scope.)

Now, the case y < x:

      insert₁ y (Cons x xs) = f x (xs, insert y xs)

    ≡   { insert₁ def. }

      (Cons x xs, insert y (Cons x xs)) = f x (xs, insert y xs)

    ≡   { generalizing (insert y xs) to ys }

      (Cons x xs, insert y (Cons x xs)) = f x (xs, ys)

    ≡   { insert.2 }

      (Cons x xs, Cons y (Cons x xs)) = f x (xs, ys)

This eliminates all free variables other than y.  Putting together
the two cases, and the earlier equation for e, we have:

    insert₁ y zs = foldL f (Nil, wrap y)
      where
        f x (xs, ys) = if y < x
                         then (Cons x xs, Cons y (Cons x xs))
                         else (Cons x xs, Cons x ys)

This completes the calculation of insert₁.