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