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.