# Fix and Mu isomorphic

In the `recursion-schemes` package the following types are defined:

``````newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)
``````

Are they isomorphic? If so, how do you prove it?

Solution

• Are they isomorphic?

Yes, they are isomorphic in Haskell. See What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package for some additional remarks.

If so, how do you prove it?

Let's begin by defining functions to perform the conversions:

``````muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
``````

To show those functions witness an isomorphism, we must show that:

``````muToFix . fixToMu = id
fixToMu . muToFix = id
``````

## From `Fix` and back

One of the directions of the isomorphism comes off somewhat more straightforwardly than the other:

``````muToFix (fixToMu t) = t
muToFix (fixToMu t)  -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t  -- See below.
t  -- LHS = RHS
``````

The final passage above, `cata Fix t = t`, can be verified through the definition of `cata`:

``````cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix
``````

`cata Fix t`, then, is `Fix (fmap (cata Fix) (unfix t))`. We can use induction to show it must be `t`, at least for a finite `t` (it gets more subtle with infinite structures -- see the addendum at the end of this answer). There are two possibilities to consider:

• `unfix t :: f (Fix f)` is empty, having no recursive positions to dig into. In that case, it must be equal to `fmap absurd z` for some `z :: f Void`, and thus:

``````cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (fmap (cata Fix) (fmap absurd z))
Fix (fmap (cata Fix . absurd) z)
-- fmap doesn't do anything on an empty structure.
Fix (fmap absurd z)
Fix (unfix t)
t
``````
• `unfix t` is not empty. In that case, we at least know that `fmap (cata Fix)` can't do anything beyond applying `cata Fix` on the recursive positions. The induction hypothesis here is that doing so will leave those positions unchanged. We then have:

``````cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (unfix t)  -- Induction hypothesis.
t
``````

(Ultimately, `cata Fix = id` is a corollary of `Fix :: f (Fix f) -> Fix x` being an initial F-algebra. Resorting directly to that fact in the context of this proof would probably be too much of a shortcut.)

## From `Mu` and back

Given `muToFix . fixToMu = id`, to prove that `fixToMu . muToFix = id` it suffices to prove either:

• that `muToFix` is injective, or

• that `fixToMu` is surjective.

Let's take the second option, and review the relevant definitions:

``````newtype Mu f = Mu (forall a. (f a -> a) -> a)

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
``````

`fixToMu` being surjective, then, means that, given any specific `Functor` `f`, all functions of type `forall a. (f a -> a) -> a` can be defined as `\alg -> cata alg t`, for some specific `t :: Fix f`. The task, then, becomes cataloguing the `forall a. (f a -> a) -> a` functions and seeing whether all of them can be expressed in that form.

How might we define a `forall a. (f a -> a) -> a` function without leaning on `fixToMu`? No matter what, it must involve using the `f a -> a` algebra supplied as an argument to get an `a` result. The direct route would be applying it to some `f a` value. A major caveat is that, since `a` is polymorphic, we must be able to conjure said `f a` value for any choice of `a`. That is a feasible strategy as long as `f`-values happen to exist. In that case, we can do:

``````fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)
``````

To make the notation clearer, let's define a type for things we can use to define `forall a. (f a -> a) -> a` functions:

``````data Moo f = Empty (f Void)

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)
``````

Besides the direct route, there is just one other possibility. Given that `f` is a `Functor`, if we somehow have an `f (Moo f)` value we can apply the algebra twice, the first application being under the outer `f` layer, via `fmap` and `fromMoo`:

``````fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
``````

Considering that we can also make `forall a. (f a -> a) -> a` out of `f (Moo f)` values, it makes sense to add them as a case of `Moo`:

``````data Moo f = Empty (f Void) | Layered (f (Moo f))
``````

Accordingly, `fromLayered` can be incorporated to `fromMoo`:

``````fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
Empty z -> \alg -> alg (fmap absurd z)
Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
``````

Note that, by doing so, we have sneakily moved from applying `alg` under one `f` layer to recursively applying `alg` under an arbitrary number of `f` layers.

Next, we can note an `f Void` value can be injected into the `Layered` constructor:

``````emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)
``````

That means we don't actually need the `Empty` constructor:

``````newtype Moo f = Moo (f (Moo f))

unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u
``````

What about the `Empty` case in `fromMoo`? The only difference between the two cases is that, in the `Empty` case, we have `absurd` instead of `\moo -> fromMoo moo alg`. Since all `Void -> a` functions are `absurd`, we don't need a separate `Empty` case there either:

``````fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
``````

A possible cosmetic tweak is flipping the `fromMoo` arguments, so that we don't need to write the argument to `fmap` as a lambda:

``````foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)
``````

Or, more pointfree:

``````foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo
``````

At this point, a second look at our definitions suggests some renaming is in order:

``````newtype Fix f = Fix (f (Fix f))

unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t
``````

And there it is: all `forall a. (f a -> a) -> a` functions have the form `\alg -> cata alg t` for some `t :: Fix f`. Therefore, `fixToMu` is surjective, and we have the desired isomorphism.

In the comments, a germane question was raised about the applicability of the induction argument in the `cata Fix t = t` derivation. At a minimum, the functor laws and parametricity ensure that `fmap (cata Fix)` won't create extra work (for instance, it won't enlarge the structure, or introduce additional recursive positions to dig into), which justifies why stepping into the recursive positions is all that matters in the inductive step of the derivation. That being so, if `t` is a finite structure, the base case of an empty `f (Fix t)` will eventually be reached, and all is clear. If we allow `t` to be infinite, however, we can keep descending endlessly, `fmap` after `fmap` after `fmap`, without ever reaching the base case.

The situation with infinite structures, though, is not as awful as it might seem at first. Laziness, which is what makes infinite structures viable in the first place, allows us to consume infinite structures lazily:

``````GHCi> :info ListF
data ListF a b = Nil | Cons a b
-- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1
``````

While the succession of recursive positions extends infinitely, we can stop at any point and get useful results out of the surrounding `ListF` functorial contexts. Such contexts, it bears repeating, are unaffected by `fmap`, and so any finite segment of the structure we might consume will be unaffected by `cata Fix`.

This laziness reprieve reflects how, as mentioned elsewhere in this discussion, laziness collapses the distinction between the fixed points `Mu`, `Fix` and `Nu`. Without laziness, `Fix` is not enough to encode productive corecursion, and so we have to switch to `Nu`, the greatest fixed point. Here is a tiny demonstration of the difference:

``````GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.
``````