Lambda the Ultimate

...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.

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, π₁(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.