What order do "least" and "greatest" refer to when talking about fixed point?

Question

In texts about fixed points in Haskell there is often mention of least and greatest fixed points. E.g. in the Data.Functor.Fixedpoint documentation or here.

Least and greatest imply an order on the involved types (or is it enough to solely define it on the fixed points?) Anyway, I never saw this order being made explicit.

What does it formally mean for a fixed point to be greater than another one in Haskell?

Calque

Answer 1

The least fixed point of a functor F is the initial algebra for F, that is, the initial object in the category of F-algebras defined by the functor. We can define a preorder on the algebras where c <= d if there is a morphism from c to d. By the definition of an initial object, there is a morphism from the initial algebra to every other algebra. That makes the initial algebra the "least" element of the defined ordering, in the sense that the initial algebra "precedes" more objects than any other object, not that nothing can precede the initial object.

Likewise, the greatest fixed point of F is the terminal coalgebra for F. A similar argument makes it the largest element in the ordering induced by morphisms in the category of F-coalgebras.

Tenantry

Being an initial object does not forbid incoming morphisms. E.g. in the category of real linear spaces, any two objects are connected by the null linear map, and that also holds for the null space (which is both initial and final in such category). In this category the induced preorder is not very meaningful, since x <= y always holds. Further, in a category multiple initial objects can exist (but must be isomorphic, so connected by morphisms). – Balder

I could have been more precise: the initial object has exactly one incoming morphism, the required identity morphism. – Tenantry

IMO, the important property of the initial algebra is not that it does not allow incoming morphisms (which might be false), but that there is a unique morphism mapping that into any other algebra. So, yes, it is the (possibly non unique) minimum in the induced ordering, but the uniqueness property is more interesting. – Balder

@Tenantry I do not think that is accurate. At the very least, it should not be true, in general, for categories with zero objects (objects which are both initial and terminal) such as the category of groups. Zero objects are initial objects. Since every zero object is also terminal, there is a morphism into them from every other object in the category. That makes me think it is not a general property of initial objects (let alone a defining property of initial objects). – Susumu

Ok, I think I figured out my confusion. If I is initial, then there is a unique morphism from I to any X. That just means the identity morphism is the only one from I -> I, not that no other morphism X -> I can exist. – Tenantry

@Tenantry That's correct. The only endo for an initial (or terminal) object is the identity. – Balder