# Exercise 3.13 ‘insert’, (way) above can be defined as an unfold. Do it. insert ∷ Ord α ⇒ α → List α → List α insert y Nil = wrap y insert y (Cons x xs) | y < x = Cons y (Cons x xs) | otherwise = Cons x (insert y xs) The hint is that the first (List α) element of the “state” tuple is the list into which to insert the maybe-wrapped second element. Once the element has been inserted, later unfold steps get Nothing. As the exercises suggests, it’s a lot easier to do this with unfoldL′. The hint gives us insert y = unfoldL′ f u where f ∷ ((List α, Maybe α) → Maybe (α, (List α, Maybe α))) u ∷ (List α, Maybe α) We have: insert' y xs = unfoldL′ ins (xs, Just y) ins (Nil, Nothing) = Nothing ins (Nil, Just x) = Just (x, (Nil, Nothing)) ins (Cons z zs, Nothing) = Just (z, (zs, Nothing)) ins (Cons z zs, Just x) | x < z = Just (x, (Cons z zs, Nothing)) | otherwise = Just (z, (zs, Just x)) This definition is a bit unwieldy! In particular, it seems a little inelegant to not be able to generate the tail (wrap x) in the second equation for ins. (Scheme's unfold, with its tail-gen procedure, can do this.) But I’m pretty sure it’s correct. We need to prove this. insert y xs = insert' y xs The proof of the above proposition is by induction on the list xs. Case Nil: insert' y Nil = { insert'.1 } unfoldL' ins (Nil, Just y) = { ins.2, unfoldL'.1 } case Just (y, (Nil, Nothing)) of Nothing → Nil Just (x, v) → Cons x (unfoldL′ ins v) = { case, pattern matching } Cons y (unfoldL′ ins (Nil, Nothing)) = { unfoldL'.1 } Cons y (case ins (Nil, Nothing) of Nothing → Nil Just (x, v) → …) = { ins.1 } Cons y (case Nothing of Nothing → Nil Just (x, v) → …) = { case, pattern matching } Cons y Nil = { wrap.1 } wrap y = { insert.1 } insert y Nil which establishes the case. For the inductive step, we need the following lemma. Lemma: unfoldL' ins (xs, Nothing) = xs The proof is by structural induction on the list xs. Case Nil: unfoldL' ins (Nil, Nothing) = { unfoldL'.1 } case ins (Nil, Nothing) of Nothing → Nil Just (x, v) → … = { ins.1 } case Nothing of Nothing → Nil Just (x, v) → … = { case } Nil which establishes the case. Case Cons y ys: unfoldL' ins (Cons y ys, Nothing) = { unfoldL'.1 } case ins (Cons y ys, Nothing) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) = { ins.3 } case Just (z, (zs, Nothing)) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) = { case, pattern matching } Cons z (unfoldL' ins (zs, Nothing)) = { hypothesis } Cons z zs which establishes the case. ∎ Case Cons z zs: insert' y (Cons z zs) = { insert'.1 } unfoldL' ins (Cons z zs, Just y) = { unfoldL'.1 } case ins (Cons z zs, Just y) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) We have two subcases to consider. Subcase y < z: = { ins.4 } case Just (y, (Cons z zs, Nothing)) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) = { case, pattern matching } Cons y (unfoldL' ins (Cons z zs, Nothing)) = { lemma } Cons y (Cons z zs) = { insert.2 } insert y (Cons z zs) Subcase y ≥ z: case ins (Cons z zs, Just y) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) = { ins.5 } case Just (z, (zs, Just y)) of Nothing → Nil Just (x, v) → Cons x (unfoldL' ins v) = { case, pattern matching } Cons z (unfoldL' ins (zs, Just y)) = { insert'.1 } Cons z (insert' y zs) = { hypothesis } Cons z (insert y zs) = { insert.2 } insert y (Cons z zs) which establishes the case. ∎ (Writing this proof revealed some mistakes in the def. of insert'!)