fixed-point-operators.md

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 andembed:

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.