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?

Sticktight

There are (observationally distinct) elements of both of those types beyond the ones you've listed. For example, Bar ⊥ ⊥ and Bar (Bar ⊥ ⊥) ⊥. I'm not sure how relevant that is to the question, though – Ensor

@DavidYoung I'm disregarding the usage of the bottom here, for it is an invalid value. – Sticktight

Well, there's your mistake: disregarding bottom. That is the core of the justification for "leftover" elements. You might want to have a look at Scott domains. – Procrastinate

@DanielWagner fix Iter and fix (join Bar) emerge from lazily evaluating the fixpoint combinator. They're not bottom. – Sticktight

@DannyuNDos I have no objection to that claim. But, believe it or not, to give a precise meaning to "lazily evaluate the fixpoint", you need bottom as a concept. – Procrastinate

For the (intricate!) maths, I'd recommend Bos & Hemerik - "An Introduction to the Category-theoretic Solution of Recursive Domain Equations". Note that the topic is indeed quite tricky: if we use data F t = K ((t->Bool)->Bool) we get a functor, and its (co)limit L should satisfy L =~ (L->Bool)->Bool) which would be impossible in the category of sets for cardinality reasons! Also, without bottoms we can not assign a value to fix (id @Bool) nor to fix not. Lazy semantics without bottoms is IMO impossible to define properly. – Casebook

@Casebook I thought the category being dealt is topological spaces? So there's no such cardinality issues. – Sticktight

Usually we take the category of DCPOs or something similar, which can be seen as topological spaces with the Scott topology. Still, that means we cannot just have "all the functions" inside A->B, but we need to restrict that set somehow (e.g. requiring continuity). – Casebook

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.

Bemuse