What is this "lax modality" business? I can sort of follow (A \lolly p) \lolly p, but not really... what do you use it for?

Actually, it feels a bit like a constructive not-not-A... how am I doing?

And you're pretty close, c.f. the continuation monad stuff below. The lax modality represents truth under an unspecified set of constraints. Computationally, it's a monadic type, so it's used to represent effects in Haskell. There are a bunch of papers you could read, including "A Judgmental Reconstruction of Modal Logic", by Pfenning and Davies.

○A

monad.

(A ⊸ p) ⊸ p

continuation monad?

□(p ∨ A)

exception monad?

damn, I feel silly for not noticing that. Does that mean that the ("parametric"?) continuation monad and exception monads are somehow "canonical enough" to stand for an arbitrary monad?

box(p + A) is not the usual exception monad -- the exception monad is usually plain old (p + A). Maybe the box is constricting how the sum gets used enough to make things work out?

Hey, a monad's a monad, right? :)

I don't know what the box is all about, either (c.f. neel's comment below). Aren't boxed things computationally something like always valuable? So box(p+A) could be sort of "totally partial" things -- things that are either a genuine A or undefined, but definitely one or the other.

By the by, just for the record... i happened to be reading this paper in the John Reynolds Festschrift called "On being a student of John Reynolds" -- the last three or so anecdotes are definitely the best -- and Andrzezzjezzezxz Fzizizlinski had the following to say:

At CMU, I found that while John's research focus had largely shifted away from continuations, he still generously let me pursue my own ideas. These eventually crystallized into an investigation of the relationship between monadic and continuation semantics, with the goal of formally establishing that, between them, first-class continuations and mutable state could simulate any other computational effect. (emphasis mine)

So if you say a computational effect is the same thing as a monad, then it sounds like you're exactly right.

Wait a minute, though - what I meant by "representing an arbitrary monad" was standing in for an abstract one with no particular equations, i.e. the circle modality. The claim about an ability to simulate any particular computation effect requires the space of so-called "computational effects" to be carefully formally delimited, and I'm curious how Filinski did that if indeed he succeeded in his programme.

Well, he has a dissertation, right? :)

FYI, ScienceDirect is giving you a bad shortcut URL to that journal issue -- it goes somewhere else instead. I can't get it to give me a good one, but you can get it by searching "John Reynolds" under "title".

You're right.. i wondered why www.cs.cmu.edu's link was wrong -- i guess it's because ScienceDirect's is!