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?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With