Premonoidal categories and notions of computation

I am currently working through Premonoidal categories and notions of computation.
Eugenio Moggi, in (Moggi 1991), advocated the use of monads, equivalently Kleisli triples, to model what he called notions of computation.
Here, we reformulate his theory. We take the base category and the category providing the denotational semantics of the extended language as primitive, and add extra structure and conditions to those and the inclusion functor of the first into the second. This more flexible and somewhat more general framework allows us to model sequential composition of programs directly by sequential composition in our extended category, rather than by a sometimes complex construction involving a monad.
As my knowledge of monads and CT is very limited, it's pretty tough... Does anybody have any opinion on the value of this paper and importance of premonoidal categories to CS?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Well, John Power...

...generally knows what he's talking about, so there's probably something interesting there.

Anyway, I'll infodump on what I know. If you take the CH isomorphism wrt to Moggi's monadic metalanguage, you learn that the type structure of the metalanguage exactly corresponds to lax logic, which is a modal logic with a single modality circle. What does this mean? The categorical semantics of the simply typed lambda calculus is a cartesian closed category, and what Moggi's metalanguage does is give a categorical semantics for lax logic -- and it says that you need a CCC with a monad.

Now, this should get you thinking about what the categorical semantics of other modal logics are. And one of the neatest results ever, imo, is that if you take a CCC with a monad and a comonad, you get a categorical model of intuitionistic S4 modal logic. This works for nearly any monad and comonad you care to pick. (There are some distributivity conditions they have to satisfy, but they're no big for any computational effect.)

And at this point, you start wanting to add additional conditions, because it's natural to want box and diamond to have a semantic relationship, too. Aleks Nanevski's thesis is the place to look -- one of his examples are exceptions, and he makes them symmetric monoidal comonads.

From nice to less nice

In the beginning there were cartesian closed categories for the semantics of the simply typed lambda calculus (with products). Environments were represented with products. Of course, we want Turing completeness so we add a fix constant but that makes things less nice; for example, we have to choose between strict and non-strict and if we choose strict we no longer have products because, π1(x,_|_) /= x. So we use a monoidal category which gives us weaker "products". Of course, we then want to add things like state, continuations, catchable exceptions, etc. We now come to another problem, what does (throw A,throw B) mean? In a monoidal category f*id;id*g = id*g;f*id (= f*g) (i.e. * is a bifunctor and this is the law that makes f*g unambiguous). If you look at the axioms for a premonoidal category, the above law is exactly what is dropped. Essentially, it forces us to always pick an order, i.e. we have to choose whether (M,N) becomes M*id;id*N or id*N;M*id. Of course, there's always a "pure" subset of a language, and this is formalized as an inclusion functor from a cartesian category and this setup is called a Freyd category. Not so incidentally, Arrows in Haskell are (almost) Freyd-categories. Freyd-categories are equivalent to kappa-categories which I believe are first mentioned here. Kappa-categories are a form of indexed categories and indexed categories are equivalent to fibrations. On a related note, reading Bart Jacob's thesis (several times) got me to have a handle on and appreciate fibrations which offer a fairly general approach to dealing with contexts and indexing. Categorical Logic and Type Theory is probably more approachable and more refined than Jacob's thesis, but it also is a heck of a lot more expensive.


...for this summary and the pointers!

I guess I will put Jacob's thesis on my read list, and if I fail to approach it, I will return to this thread.