## Exercise 3.21 Express ‘unfoldN’ in terms of ‘unfoldN′’ and vice versa. (a) unfoldN as an instance of unfoldN′ We need a definition of the form unfoldN p f x = unfoldN′ g x First, assume p x = True: unfoldN p f x = unfoldN′ g x ≡ { unfoldN.1, p x = True } Zero = unfoldN′ g x ≡ { unfoldN′.1 } Zero = case g x of Nothing → Zero ... Requiring that p x ⇒ g x = Nothing gives us a solution for this case. In the case p x = False: unfoldN p f x = unfoldN′ g x ≡ { unfoldN.1, p x = False } Succ (unfoldN p f (f x)) = unfoldN′ g x ≡ { unfoldN′.1 } Succ (unfoldN p f (f x)) = case g x of Nothing → Zero Just y → Succ (unfoldN′ g y) ≡ { define: not (p x) ⇒ g x = Just (f x) } Succ (unfoldN p f (f x)) = case Just (f x) of Nothing → Zero Just y → Succ (unfoldN′ g y) ≡ { case, pattern matching } Succ (unfoldN p f (f x)) = Succ (unfoldN′ g (f x)) I guess we could use a coinduction hypothesis to show that this equation holds? After this not-quite-rock-solid derivation, we have: unfoldN p f = unfoldN′ g where g x = if p x then Nothing else Just (f x) (b) unfoldN′ as an instance of unfoldN We can use the universal property of unfoldN here: unfoldN′ f = unfoldN p g iff unfoldN′ f x = if p x then Zero else Succ (unfoldN′ f (g x)) We need to consider two cases. Case f x = Nothing: unfoldN′ f x = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { unfoldN′.1 } (case f x of Nothing → Zero Just y → Succ (unfoldN′ f y)) = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { f x = Nothing, case, pattern matching } Zero = if p x then Zero else Succ (unfoldN′ f (g x)) Defining p x | f x == Nothing = True ... gives us a solution to this case. Case f x = Just y: unfoldN′ f x = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { unfoldN′.1 } (case f x of Nothing → Zero Just z → Succ (unfoldN′ f z)) = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { f x = Just y } (case Just y of Nothing → Zero Just z → Succ (unfoldN′ f z)) = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { case, pattern matching } Succ (unfoldN′ f y) = if p x then Zero else Succ (unfoldN′ f (g x)) ≡ { define: f x = Just y ⇒ p x = False, ITE } Succ (unfoldN′ f y) = Succ (unfoldN′ f (g x)) Defining g x = y gives us a solution in this case. We have: unfoldN′ f = unfoldN p g where p x | f x == Nothing = True | otherwise = False g x = case f x of -- the ‘Nothing’ case can’t happen Just y → y This definition is a little awkward. As is typically the case with defining boolean-based unfolds in terms of Maybe-based functions, we need to derive two functions from one. The result is apparent redundancy. Note that g is only invoked if (f x) is a Just value. We could use a library function to define, equivalently, g = fromJust ∘ f