hunting for (monads with) take-out, pt 1

Monads abstract many different kinds of phenomena. One class of phenomena comes under the heading "control", such as the continuations-based monads; another comes under the heading "collection", such as List, Set, ... . Both of these aspects of computation share a common property -- which is whether they support take-out. It's easiest to grasp this property in terms of the collection-based interpretation of monads. If you put a widget into a list, in most cases you can get it out again. The Option monad (aka Maybe aka Lifting) is the simplest form of this basic behavior. If you put something into Option, you can get it out. However, if someone (or some computation) hands you an Option, you don't know if you can get anything out until you try. (This, by the way, illustrates a basic counting principle: there are more ways to put something into a collection and then take something out, than there are to take something out and put something in. This principle -- as John Baez pointed out in his presentation at GroupoidFest '08 -- shows up in some surprising places that we will return to later.)

So, Option, List, Set and the like support a weak form of take-out. Other monads, such as Haskell's IOMonad, are notoriously "sticky". Code goes in, but values don't come out. Monads that don't support take-out typically have a flavor of transactions with no compensating action. After you press the armageddon button you typically don't get an undo option, or even a "make good" option. Error monads can have this flavor.

Recently, i was helping someone understand the stickiness of the IOMonad and the question came up, what sort of properties would be necessary to guarantee a take-out option? Since i have often pondered this question, i resolved to work this out for myself. Communications with various and sundry at the Haskell-cafe gathered suggestions to try using a co-monad, but that really turns into a suggestion to find a monad that simultaneously (and canonically) supports a co-monad structure. This helps as an abstract spec, but at the time, it didn't give me a concrete construction.

Then i remembered that linearity would give me this property that every "put-in" would be matched by a "take-out" and vice versa. So, the question became out to line up the smallest interpretation of linear logic with a monad. That is, we are looking for a category the objects of which interpret the linear formulae (aka types), and the morphisms of which represent programs. If we started with some monoidal structure to interpret the multiplicative "and" (aka tensor), then can we interpret the monoidal structure as if it were a collection and derive the monad structure from the collection.

In the next post we'll take a look at what this all means. In fact, what we'll do is show how to relate the linear structure of a compact closed category to the structure of a monad with take-out.