Greatest and Least Fixed Points

I've recently stumbled upon a goldmine of amazingness in computer science and math. Combinatorial species, categorical treatments of computation, and many different strange things we can do in Haskell's type system and with the extensions to the type system.

One of these things is to have types that take fixed points of other types. This seemed very strange to me at first, and I've only just now understood the difference between the greatest and least fixed point of a type declaration. Thank you "A Neighborhood of Infinity" for being such an enlightening source of math and computer science knowledge!

As I understand them, polynomial types are of the form c1*X^n1 + c2*X^n2 + ... cN*X^nN, ci >= 0, ni >= 0. Since Haskell allows multiple type constructors, separated by pipes (|), the type systems admits "sum" types. A sum type is either one of the type on the left of the + or one of the type on the right. Each constructor (where the name is the tag, making the sum a disjoint (tagged) union) is isomorphic to an n tuple. This is a product type, where a product type is a pairing of one of the thing to the left of the * and one of the type to the right of the *.
It is interesting to note that we can also do composition of types, such as [(a,b)], where we are composing list with a product of types a and b. This means that the only operations from the theory of combinatorial species that Haskell does not have are differentiation and functorial composition. Of course, there are libraries for the creation of these kind of types, but I'm specifically talking about encoding them directly in Haskell as types, not as data.

One more thing before I get to the point of all of thing is that the Either type in Haskell is a value level sum, and comma (,) is a value level product.

So! Fixed points! If we consider the list type LA = 1 + X*LA, which is lists over a type A, we may want to solve for LA. What finally cleared up the idea of greatest and least fixed points for me was that this type can have two meanings, one which is "smaller" than the other. The "smaller" meaning is that of finite lists- a list is either an empty list or a thing paired up with a finite list. The "larger" meaning (the meaning that admits larger values) is that a list is either empty or a thing paired with a possibly finite list. This allows infinite lists (which is what Haskell means by a list). I was reading a paper by Wadler that make use of the idea of the least fixed point, and I completely missed out on the fact that he was using this idea to make sure that all the structures that he was talking about were finite.

There is one more thing that is interesting to note about this idea. In Haskell we can legally write this type:

data mu p = In (p (mu p))

I still don't know why they use mu to denote this "least fixed point" type, nor why the type constructor is called In (is it related to the in operator used to come out of a functor structure in a F-algebra, which is given the same name? I think it might be). The point here is that we then define something like this:

data Val a = Val Int

data Add e = Add e e

We can then create a sum type out of Val and Add, and create an Expr type mu Expr which takes the least fixed point of the sum type. They we can create an evaluator for this type. The nice thing about working this way is that we can construct types out of other types, and be explicit in the type signature about what sorts of things we admit in the resulting type. This is all describe in the paper "Data Types a la Carte" by Wouter Swierstra.

Okay, that is enough for now. I am still learning this material, and it is way beyond me in many ways, so there may be abuses of terminology and mistakes of understanding in the above post, so beware!