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

Question

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?

Answer 1

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.