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