## Exercise 3.22 What is the universal property of ‘unfoldN’? Presumably, it’s h = unfoldN p f iff h x = if p x then Zero else Succ (h (f x)) for all h ∷ α → Nat. For the fusion law, we expect it to be similar to that for list unfold: (unfoldN p f) ∘ g = unfoldN p' f' With the universal property, we have (unfoldN p f) ∘ g = unfoldN p' f' iff ((unfoldN p f) ∘ g) x = if p' x then Zero else Succ (((unfoldN p f) ∘ g) (f x)) Given p' x = True, we (try to) reason: ((unfoldN p f) ∘ g) x = Zero ≡ { application, unfoldN.1 } if p (g x) then Zero else ... = Zero Defining p (g x) ⇒ p' x gives us a solution here. In the case p' x = False, we have: ((unfoldN p f) ∘ g) x = Succ (((unfoldN p f) ∘ g) (f' x)) ≡ { application, unfoldN.1 } if p (g x) then Zero else Succ (unfoldn p f (f (g x))) = Succ (((unfoldN p f) ∘ g) (f' x)) ≡ { application } if p (g x) then Zero else Succ (unfoldN p f (f (g x))) = Succ (unfoldN p f (g (f' x))) ≡ { define: p' x = False ⇒ p (g x) = False } Succ (unfoldN p f (f (g x))) = Succ (unfoldN p f (g (f' x))) ≡ { unapplying Succ from both sides } unfoldN p f (f (g x)) = unfoldN p f (g (f' x)) which gives us f ∘ g = g ∘ f'. From the constraints on p', we also define: p' = p ∘ g So (unfoldN p f) ∘ g = unfoldN p' f' holds if (p' = p ∘ g) ∧ (f ∘ g = g ∘ f') for all p, f, g, p', and f' of the appropriate types. This is quite similar to the fusion law for list unfold.