Least fix point, greatest fix point

Question

How come the least fix point coincides with the greatest fix point in a lazy non-total language like Haskell. What does continuity on complete partial orders have to do with that?

Answer 1

In a CPO (which we interpret a type as), any increasing chain has a least upper bound.

Here's an example that should convey the intuition why, in the domain of CPOs, least fixed points and greatest fixed points coincide. Consider the following functor, abusing the list notation for conciseness:

data ListF a x = [] | a : x

Its greatest fixed point is the type of Haskell lists (possibly infinite, possibly partial). What about its least fixed point? The following elements must be in it (Fix constructors are omitted):

0 : _|_
0 : 1 : _|_
0 : 1 : 2 : _|_
...

And they form an increasing chain, so there must be a least upper bound, which has to be the infinite list of natural integers 0 : 1 : 2 : .... So the least fixed point of ListF contains infinite lists, and consequently coincides with the greatest fixed point.

---

As was pointed out in the comments, the claim that the greatest fixed point is given by the type [] may need clarification. For instance, wouldn't some CPO "BigList" of lists indexed by large ordinals make an even greater fixed point?

One can first show that [] satisfies the definition of a final ListF-coalgebra. Then, a property of final coalgebras is that they are unique up to isomorphism. Therefore, lists indexed by larger ordinals would result in a non-isomorphic CPO, so that cannot be a final coalgebra.

I could stop there, but hold on, isn't BigList still a greater fixed point of ListF? My conclusion is to chalk the issue up to bad terminology and formally we should only discuss "final coalgebras", and not "greatest fixed points".

Depending on how you define a "fixed point" of a functor in CPO and a notion of (pre)order between CPOs, you may find that BigList is a fixed point of ListF, that it is greater than [], that you run into set-theoretic paradoxes when reaching towards the "greatest fixed point", and that ultimately there is nothing of value to Haskell practitioners in that way of formalizing a "greatest fixed point" because you actually wanted the nice properties of a final coalgebra.

(I'd be interested to know of a direct way to define "fixed point" that excludes BigList as one.)

So instead, the term "greatest fixed point" might as well be a synonym for "final coalgebra". Some intuition carries over ("fixed points" can commonly be approached by iteration), some doesn't (it's not "greatest" in a set-theoretic sense).