Instantly share code, notes, and snippets.

# fixed-point operators

In general, finds the “fixed point” of some endofunctor, which means some type `t`, such that `f t ~ t`. The simplest operator is often called `Fix`, and takes advantage of a language’s primitive recursion to provide a very straightforward definition:

`newtype Fix f = Fix { unfix :: f (Fix f) }`

There are some problems with this, however:

1. most languages provide general recursion (and, in fact, this definition requires it), so such a definition can’t be total; and
2. this definition can have different semantics in different languages – e.g., in Scala, it would be strict (and therefore finite), while in Haskell the recursion would be lazy, and thus potentially infinite.

There are (at least) a pair of other operators that give more principled and consistent semantics.

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

data Nu f where
Nu :: (a -> f a) -> a -> Nu f```

`Mu` defines a recursive structure as a fold, and it’s apparent from the definitions of `cata` and`embed`:

```cata :: (f a -> a) -> Mu f -> a
cata φ (Mu f) = f φ

embed :: f (Mu f) -> Mu f
embed fm = Mu (\f -> f (fmap (cata f) fm))```

`cata` simply applies the fold in `Mu` to the provided algebra, and `embed` adds another step to the fold in `Mu`.

This provides a structure that is always strict and finite – the “least” fixed-point.

`Nu`, on the other hand, is for defining the “greatest” fixed-point, which includes potentially-infinite values in addition to the finite values covered by `Mu`. It subsumes all of `Mu`’s values (hence the terms “greatest” and “least”), and it’s trivial to define `Mu f -> Nu f` … but that discards the proof that the value is finite, and so folding it can no longer be guaranteed to terminate.

Looking at `Nu`’s structure, you can see it holds both a coalgebra (`a -> f a`) to unfold a single step, and a seed value to be passed to that algebra. It’s the delayed application of the seed to the algebra that makes `Nu` lazy, and therefore capable of representing infinite values.