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?

Agate

Can you elaborate? Are you talking about fixed points at the term level (e.g. recursive functions) or at the type level (recursive types)? Also note that in a CPO with bottom every continuous function has a least fixed point, but can have no greatest fixed point (id @Bool only has least = bottom). (Further, if generalized a bit, this might be more in scope at CS.SE instead of SO -- even if the Haskell community has a broadish scope here on SO, and on CS.SE the community is not that large.) – Change

At the type level, the fix point of a functor. I find this mentioned in various places, in schoolofhaskell.com/user/edwardk/moore/for-less or in cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf , but I can't make a picture – Agate

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).

Cymar

I'm unsatisfied by this answer -- the topic is non trivial, and would require a proper proof. For instance, even in the list example above, why couldn't the final coalgebra contain, beyond the lists mentioned above, some "longer" sequence as well? By longer, here, I mean a larger ordinal. The result might depend on the category at hand, or on some assumptions on the functor -- it's hard to see unless a painful formalization is done (IMO). – Change

The Wikipedia CPO page you link to opens by saying three are three different definitions that are referred to as CPOs. It might improve the answer if you say which one you're talking about. – Terreverte

@Terreverte The link was added by someone else, and all of the definitions imply the property I stated upfront, and that is also all I need in my answer, so it doesn't seem helpful to tell apart this or that flavor of CPO. But this is exactly the definition of omega-cpo (the third one), and the article mentions that the first two are strictly finer notions. – Cymar

@Change It's not that painful to check that [] is a final coalgebra, which is then unique up to isomorphism. I just edited my answer to expand on that point. – Cymar

Thanks. Set paradoxes can probably be avoided if one takes the category of CPOs whose cardinality is <= some given cardinal. Even there, perhaps [] indeed turn out to be the final coalgebra, and that the unique morphism from a "big list" to [] is the truncation to the first omega elements. – Change