# What's the intuition behind fixpoints of monads NOT being the direct limit?

Consider the following datatype:

``````data Foo = Halt | Iter Foo
``````

This is the fixpoint of `Maybe`. It contains the direct limit of the sequence `Void`, `Maybe Void`, `Maybe (Maybe Void)` and so on, where `pure` is the injecting morphism. However, `Foo` has an element not covered by the direct limit, namely `fix Iter`.

Let me have another example:

``````data Bar = Bar Bar Bar
``````

This is the fixpoint of `Complex`. Since `Void`, `Complex Void`, `Complex (Complex Void)` and so on are all homeomorphic to `Void`, the direct limit is also `Void`. However, `Bar` has an element, namely `fix (join Bar)`.

So what's the mathematical justification of those "leftover" elements?

Solution

• As was pointed out in the comments, these elements exist as a consequence of nontermination.

In a terminating language, or equivalently, in the category of sets, the initial algebra (least fixed point) of `Maybe` is `Nat` and the initial algebra of `Complex` (`data Complex a = Complex a a`) is the empty type `Void`. `fix Iter` and `fix (join Complex)` don't exist because `fix` is not definable in a terminating language.

With unrestricted nontermination, sets are no longer a good model of types because the infinite loop inhabits all types. A common alternative in that case are DCPOs or some similar order structure. In particular, the existence of bottom and of limits for increasing sequences are just what is needed to be able to define `fix` (via Kleene's theorem). So for example, in the case of `data Nat = Z | S Nat`, `fix S` is obtained as the limit of the sequence `⊥`, `S ⊥`, `S (S ⊥)`, `S (S (S ⊥))`, etc.

You do need to be careful about where the bottoms are. For example, in Haskell, `Maybe a` is a DCPO consisting of `⊥`, `Nothing`, and `Just x` for `x` an inhabitant of `a`. You can also define a strict variant:

``````data SMaybe a
= Nothing
| Just !a
``````

which as a DCPO contains `⊥`, `Nothing`, and `Just x` for `x` a non-bottom inhabitant of `a`. In particular, the sequence `⊥`, `Just ⊥`, `Just (Just ⊥)`, etc. is no longer well-defined (or if you really want to give it a value, it would be constantly equal to `⊥`), so you no longer get a way to construct an infinite sequence of `Just`, and indeed the initial algebra (least fixed point) of `SMaybe` only contains finite sequences of `Just`/`S` applied to `Nothing`/`Z`, and `⊥` alone.

Note that this is not restricted to lazy languages. DCPOs serve just as well to model strict languages. It's just that there is an explicit distinction between values and computations which makes things more obvious in a way. For example, the option type in ML

``````type 'a option = None | Some of 'a
``````

corresponds to the set of values consisting of `None` and `Some x` for `x` in `'a`. But the type `unit -> 'a option` is not a pure function from `unit` values to `'a option` values. It is a function from `unit` to computations with result `'a option`. A computation with result type `t` denotes an element of the lifted type `{⊥} + t` (i.e., either bottom or a value in `t`). So you can use `unit -> _` as a type of thunks and encode everything that's going on in Haskell in a strict language.