Lambda the Ultimate

For those of you still looking, here's a fun introduction to Category Theory by Barry Mazur.

The Haskell Programmer's Guide to the IO Monad - Don't Panic. Stefan Klinger.

Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the non-functional IO actions ---which do have side effects--- from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge?

This report scratches the surface of category theory, an abstract branch of algebra, just deep enough to find the monad structure. On the way we discuss the relations to the purely functional programming language Haskell. Finally it should become clear how the IO monad keeps Haskell pure.

It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written.

The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory.

While some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding).

Combining computational effects: commutativity and sum

We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's side-effects monad transformer (an application is the combination of side-effects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).

A longer version: Combining Effects: Sum and Tensor

B. Jacobs, Distributive laws for the Coinductive Solution of Recursive Equations, Information and Computation, to appear.

This paper illustrates the relevance of distributive laws for the solution of recursive equations, and shows that one approach for obtaining coinductive solutions of equations via infinite terms is in fact a special case of a more general approach using an extended form of coinduction via distributive laws...

Turi and Plotkin first investigated such a situation where one functor G describes the syntax of a programming language and the other functor F the behaviour of programs (terms) in that language. Having a distributive law GF => FG means that the behaviour on terms is well-defined, and leads to results like: (coalgebraic) bisimilarity is an (algebraic) congruence. Hence distributive laws capture where "algebra meets coalgebra".

Interesting stuff.

Be warned: This paper is highly technical, and requires familiarity with the fundamental notions of category theory.

B. Jacobs, A Bialgebraic Review of Regular Expressions, Deterministic Automata and Languages, Technical Report ICIS-R05003, Institute for Computing and Information Sciences, Radboud University of Nijmegen.

This papers reviews the classical theory of deterministic automata and regular languages from a categorical perspective. The basis is formed by Rutten's description of the Brzozowski automaton structure in a coalgebraic framework. We enlarge the framework to a so-called bialgebraic one, by including algebras together with suitable distributive laws connecting the algebraic and coalgebraic structure of regular expressions and languages. This culminates in a reformulated proof via finality of Kozen's completeness result. It yields a complete axiomatisation of observational equivalence (bisimilarity) on regular expressions. We suggest that this situation is paradigmatic for (theoretical) computer science as the study of "generated behaviour".

Bart Jacobs. Bialgebras. Enough said.

This paper was mentioned here before, but not on the home page.

It deserves to get more attention, since it is quite cool.

Warning: This one isn't for the faint of heart, and uses scary terms like polynomial functors, initial algebras and terminal coalgebras, constructive set theory and more...

For those who do not think that "catamorphism" sounds scary, Generic Accumulations paper presents a new flavor of fold: fold with accumulators (afold).

You might be acquainted with its cousin - pfold, or fold with parameters. Both come from the family of comonadic fold.

A homepage of Alberto Pardo contains more information on them.

PS: if you are new to fold or bananas/lenses, LtU papers page has a couple of introductory links.

Datatype Laws without Signatures

Using the well-known categorical notion of `functor' one may define the concept of datatype (algebra) without being forced to introduce a signature, that is, names and typings for the individual sorts (types) and operations involved. This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra.

Does it sound like "a module without a signature"?

If you like programming with bananas, lenses, and other weird things you might like this paper as well.

PS: OTOH, if you are sceptic about bialgebraic programming, then dialgebraic is definitely not for you.

From the discussion group:

For those interested in a brief introduction to category theory, James Cheney has recently posted some PDF slides titled Category Theory for Dummies on his home page.

These slides are introductory, and don't contain advanced techniques, but they seem to be nicely done.

The list of accepted papers and the abstracts of invited talks are now available.

Warning: This gathering is not for the faint of heart...