[SOLVED] Fix and Mu isomorphic

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.

Addendum

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.

Fix and Mu isomorphic

From Fix and back

From Mu and back

Addendum

From `Fix` and back

From `Mu` and back