Inspired by the discussion on comonads we had two weeks ago I gave a little tutorial on monads and comonads which was finished off by Neil.
A standard example for monads are arising from substitution: Consider a the set of terms given by an endofunctor . Terms over a given set of variables can be encoded as and this gives rise to a monad, where embedding variables into terms and corresponds to applying a substitution given by .
Dually, we construct a comonad which corresponds to infinite terms with labels, the counit returns the top-level label and relabels a tree according to a relabelling function . The example of streams which inspired this little tutorial is an instance of this, if we choose , i.e. the identity functor, since .
Neil explained that the monad is the free monad over , i.e. this is given by applying the left adjoint of the forgetful functor from the category of monads to the category of endofunctors, dually is the cofree comonad. Neil and his student Fed also investigated the monad which is the fully iterative monad over . However, it seems that its dual has not yet attracted much attention.