Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?

like image 748
michid Avatar asked May 13 '20 20:05

michid


1 Answers

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.

like image 70
chepner Avatar answered Sep 27 '22 22:09

chepner