## 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.