# Exercise 3.6
(a) Express unfoldL in terms of unfoldL′.
We seek solutions for h and u in
unfoldL p f g b = unfoldL' h u
b and u both denote the first seed, so we say b = u.
We reason that (h u) should yield Nothing when (p b) is true:
h u = if p b then Nothing else ...
In unfoldL, the next consed-on value is (f b) and the next seed is
(g b). Since f returns a tuple of these values wrapped in a Maybe,
we reason:
h u = if p b then Nothing else Just (f b, g b)
So we have
unfoldL p f g b = unfoldL' h b
where
h u = if p b then Nothing else Just (f b, g b)
We prove that this definition is equivalent by case analysis.
Case (p b) = True:
unfoldL' h b
= { unfoldL'.1 }
case f u of
Nothing → Nil
...
= { definition of f above }
case (if p b then Nothing else Just (f b, g b)) of
Nothing → Nil
...
= { (p b) = True }
case Nothing of
Nothing → Nil
...
= { case }
Nil
= { unfoldL.1, (p b) = True }
unfoldL p f g b
Case (p b) = False. We will use the (co?)induction hypothesis,
unfoldL' h (g b) = unfoldL p f g (g b)
though I'm not sure whether this is the right form for such a thing.
FIXME: We can just define unfoldL' h = unfoldL p f g, I think.
unfoldL' h b
= { unfoldL'.1 }
case f u of
Nothing → Nil
Just (x, v) → Cons x (unfoldL′ f v)
= { def. of f above }
case (if p b then Nothing else Just (f b, g b)) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL′ f v)
= { p b = False, if }
case Just (f b, g b) of
Nothing → Nil
Just (x, v) → Cons x (unfoldL′ f v)
= { case, pattern-matching }
Cons (f b) (unfoldL' f (g b))
= { hypothesis }
Cons (f b) (unfoldL p f g (g b))
= { unfoldL.1, p b = False }
unfoldL p f g b
which establishes the case. ∎
(b) Express unfoldL′ in terms of unfoldL.
Jumping ahead slightly, we use the universal property of unfoldL:
unfoldL' f' = unfoldL p f g
iff
unfoldL' f' b = if p b then Nil else Cons (f b) (unfoldL' f' (g b))