## Exercise 3.25 Deforest the following: hyloN' :: (Maybe a -> a) -> (a -> Maybe a) -> a -> a hyloN' f g = foldN' f . unfoldN' g We'd like to calculate a new definition for hyloN' that does not use foldN' or unfoldN'. We'll try to proceed by case analysis on g in the expression: hyloN' f g x = case g x of ... Case g x = Nothing: hyloN' f g x = foldN' f (unfoldN' g x) ≡ { unfoldN'.1 } hyloN' f g x = foldN' f (case g x of Nothing -> Zero Just y -> Succ (unfoldN' g y)) ≡ { g x = Nothing, case } hyloN' f g x = foldN' f Zero ≡ { foldN'.1 } hyloN' f g x = f Nothing which gives a value for this case: hyloN' f g x = case g x of Nothing -> f Nothing -- ... This looks slightly redundant. Case g x = Just y: hyloN' f g x = foldN' f (unfoldN' g x) ≡ { unfoldN'.1 } hyloN' f g x = foldN' f (case g x of Nothing -> Zero Just y -> Succ (unfoldN' g y)) ≡ { g x = Just y, case, pattern matching } hyloN' f g x = foldN' f (Succ (unfoldN' g y)) [where y = fromJust (g x)] ≡ { foldN'.1 } hyloN' f g x = f (Just (foldN' f (unfoldN' g y))) [where y = fromJust (g x)] ≡ { unapply, rewrite as composition } hyloN' f g x = f (Just ((foldN' f ∘ unfoldN' g) y)) [where y = fromJust (g x)] ≡ { specification } hyloN' f g x = f (Just (hyloN' f g y)) [where y = fromJust (g x)] which gives a solution for this case. hyloN' f g x = case g x of Nothing -> f Nothing Just y -> f (Just (hyloN' f g y)) This completes the calculation.