Archive for December, 2005

monads and comonads

Friday, December 16th, 2005 by Thorsten

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 \mu X.F\,X given by an endofunctor F. Terms over a given set of variables can be encoded as M_F\,X = \mu X.X + F\,X and this gives rise to a monad, where \eta \in X \to M_F\,X embedding variables into terms and \hat{f}\in M_F\,X\to M_F\,Y corresponds to applying a substitution given by f\in X\to M_F\,Y.

Dually, we construct a comonad C_F\,Y = \nu X.Y\times F\,X which corresponds to infinite terms with labels, the counit \epsilon \in M_F\,X \to X returns the top-level label and \check{f}\in C_F\,X \to C_F\,Y relabels a tree according to a relabelling function f \in X \to C_F\,Y. The example of streams which inspired this little tutorial is an instance of this, if we choose F\,X=X, i.e. the identity functor, since C_F\,Y = \nu X.Y\times X \simeq \mathbb{N}\to Y.

Neil explained that the monad M_F is the free monad over F, 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 C_F is the cofree comonad. Neil and his student Fed also investigated the monad M^*_F\,Y=\nu X.Y + F\,X which is the fully iterative monad over F. However, it seems that its dual C^*_F\,Y=\mu X.Y\times F\,X has not yet attracted much attention.

Solving Sudoku a la Bird

Friday, December 9th, 2005 by Graham

I gave an overview of a Haskell approach to solving Sudoku puzzles, based upon lecture notes from Richard Bird. The approach is classic Bird: start with a simple but impractical solver, whose efficiency is then improved in a series of steps. The end result is an elegant program that is able to solve any Sudoku puzzle in an instant. It’s also an excellent example of what has been termed “wholemeal programming” — focusing on entire data structures rather than their elements. I’m planning on teaching this as part of the new Advanced Functional Programming module next semester.

Containers: Who they? What do? and Why?

Friday, December 9th, 2005 by Peter

I gave a quick guide to a Containers view of parametrised datatypes. With the aid of a couple of examples I introduced the notion of shapes (Nat for lists as the shape of a list is simply it’s length) and positions (indicies where data can be stashed, for lists this is the finite sets Fin). I showed how containers are closed uder Disjoint Union and Cartesian Product, and Least Fix-point if we have W-Types (thus illustrating that the shape of a tree container is a tree with no data in it). I also introduced container morphisms and mentioned that they correspond exactly to natural transformations or polymorphic programs in Haskell.

Thinking about datatypes in this way gives us a number of benefits, for instance some calculations on Data-Types, such as the derivative, fit very nicely into the framework of containers. It is partly for this reason that we are thinking of using an extension to the containers in the above (sorted containers) as datatypes in Epigram2.

Visitors from Sheffield

Saturday, December 3rd, 2005 by Graham

Mike Stannett and Simon Foster visited from Sheffield today, and gave a talk about a new approach to understanding monads. There was also some discussion about co-monads, in particular the stream co-monad.