Monads Model Substitution ------------------------- This is from Rydeheard and Burstall's article in Nivat and Reynolds "Algebraic Methods in Semantics". I think there are other categorical ways to model substitution, but this is pretty cool. Suppose T constructs terms from variables: TA = A + (plus TA TA) + (times TA TA) T builds terms from variables. If Var = {A, B, C} then TVar = {A, (plus A A), (times (plus B C) A), ...} Then we have unit : A -> TA is the leftmost inject (make a term from a variable) and join : TTA -> TA is substitution. For example, (plus {(plus A B)} {C}) becomes (plus (plus A B) C). Terms over terms over variables become terms over variables. Oddly, in "terms over terms", the variables seem to have disappeared. Monad algebras and Eilenberg-Moore ---------------------------------- From there, it's easy to go to the Eilenberg-Moore construction of an adjunction from a monad. An _algebra_ of a monad is an object A and an evaluation map eval : TA -> A that respects unit and join. For example, for the term monad, we could take A to be natural numbers and evaluate terms. For any monad T and object A, we can form the _free algebra_ of T on A as follows. We let X = TA. Then join : TX -> X is evaluation. Note that X is the free T-algebra, not TX. For the term monad, X is just the set of terms over A. The free algebra is initial in the category of T-algebras. If T is a monad on a category C, the adjunction is between C and C^T, where C^T is the category of T-algebras on C. One way maps an algebra to its underlying object, and the other way constructs the free T-algebra over an object. The unit of the adjunction is the monad unit. Least fixed points ------------------ This is from Barr and Wells "CT for CS", Arbib and Manes "Algebraic approaches to program semantics", or even Pierce. Let's do the initial algebras of a functor that doesn't necessarily have a monad attached. Let FA = Num + (plus A A) + (times A A) This is different from before, because F is no longer recursive (and we put numbers in -- the reason becomes clear in a second). So there's no way to define join : FFA -> FA. We can still form F-algebras, no problem. For instance, take A to be Num and eval : FA -> A to be evaluation. But it's not as fun as before. It's not hard to show that if (X, eval : FX -> X) is initial in the category of F-algebras, then eval is an isomorphism. So we get an isomorphism between FX and X, that is, a fixed point of F. For F above, that's the set of terms over numbers. We can construct fixed points by approximation. If F is cocontinuous (preserves colimits), the fixed point is also the colimit of the diagram i Fi FFi FFFi 0 -> F0 -> FF0 -> FFF0 -> ... where i is the unique arrow from 0 to F0. For example, if FA = X + X*A Ff = id + id*f we get 0 -> X -> X + X*X -> X + X*X + X*X*X -> ... We get more and more information moving left to right. Greatest fixed points --------------------- This is from Arbib and Manes, who published it first. Taking the greatest fixed point is equally fun. If F is co-continuous, it's the limit of FFFt FFt Ft t ... -> FFF1 -> FF1 -> F1 -> 1 where t is the unique arrow from F1 to 1. For the same F, it's ... -> X*X*X + X*X + X -> X*X + X -> X -> 1 We get less and less information left to right. It's neat to see how the arrows work (but too hard to write in ascii). The difference between least and greatest is that the least fixed point, since it's built from "below", allows only finitely many X's, while the greatest allows infinitely many. I.e. streams versus lists. The greatest fixed point is probably terminal in the category of co-algebras A -> FA (check A&M). T-Algebras vs. F-Algebras ------------------------- It seems to me that they're used in totally different situations. F-algebras model fixed points, while T-algebras model substitution. It's easy to write down a fixed point for a monad. It's just TA. It's harder for a functor. Also, monads yield an algebra _over an object_, which is more general. Fixed points for monads means that TA and TTA are isomorphic, with join_A : TTA -> TA and unit_TA : TA -> TTA as inverses, which is true from the monad laws. The free monad over a functor ----------------------------- Given a functor F and a natural transformation u : I -> F, we can build a free monad T from F as the limit of u Fu FFu I -> F -> FF -> FFF -> ... This limit is in the category of functors and natural transformations. The construction, as given in Rydeheard and Burstall, is rather complicated. If FA = A + (plus A A) + (times A A) then TA = A + (plus TA TA) + (times TA TA) is the free monad over F. Unit is left injection, and Join is substitution. So that finishes the connection between the two.