haskellrecursion-schemesfixpoint-combinators# Fix and Mu isomorphic

## From

## From

## Addendum

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

`Fix`

and backOne 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.)

`Mu`

and backGiven `muToFix . fixToMu = id`

, to prove that `fixToMu . muToFix = id`

it suffices to prove either:

that

`muToFix`

is injective, orthat

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

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code