## Exercise 3.10

‘deleteL’ is a paramorphism.  Redefine it using ‘paraL’.

We seek a solution to the following for all finite lists xs:

    deleteL y = paraL f e

Going by the type of paraL, we have the type signatures

    f ∷ α → (List α, List α) → List α
    e ∷ List α

First, the case Nil.

      paraL f e Nil = deleteL y Nil

    ≡  { deleteL.1, paraL.1 }

      e = Nil

which is our first solution.  Continuing, the non-empty case gives
us two subcases.

Case (Cons x xs), subcase y == x:

      paraL f e (Cons x xs) = deleteL y (Cons x xs)

    ≡   { deleteL.2 }

      paraL f e (Cons x xs) = xs

    ≡   { paraL.2 }

      f x (xs, paraL f e xs) = xs

    ≡   { generalizing (paraL f e xs) to ys }

      f x (xs, ys) = xs

Case (Cons x xs), subcase y ≠ x:

      paraL f e (Cons x xs) = deleteL y (Cons x xs)

    ≡   { deleteL.2 }

      paraL f e (Cons x xs) = Cons x (deleteL y xs)

    ≡   { paraL.2 }

      f x (xs, paraL f e xs) = Cons x (deleteL y xs)

    ≡   { hypothesis: paraL f e xs = deleteL y xs, generalize to ys }

      f x (xs, ys) = Cons x ys

which gives the remaining solution for f.  Putting it all together,
we have:

    deleteL y = paraL f Nil
      where f x (xs, ys) = if y == x
                             then xs
                             else Cons x ys

This completes the synthesis.