Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

 [ website | My Website ] [ userinfo | livejournal userinfo ] [ archive | journal archive ]

[Jun. 4th, 2007|09:16 pm]
Jason
 [ Tags | work ]

Had a good chat with in the grad lounge around lunchtime about his and my research stuff. He told me about several surprising encodings of the lax modality ○. Apparently ○A is equivalent to both (A ⊸ p) ⊸ p and □(p ∨ A) for some fresh propositional atom p ... at least the latter encoding works if you also hereditarily box everything else in sight.

Feeling sort of sniffly and sore-throated, though. I hope I haven't caught the latest cold that's going around.

 From: 2007-06-05 02:54 am (UTC) (Link)
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?
 From: 2007-06-05 02:55 am (UTC) (Link)
Actually, it feels a bit like a constructive not-not-A... how am I doing?
 From: 2007-06-08 08:59 am (UTC) (Link)
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.
 From: 2007-06-05 06:19 am (UTC) (Link)
○A

(A ⊸ p) ⊸ p

□(p ∨ A)

 From: 2007-06-05 01:19 pm (UTC) (Link)
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?
 From: 2007-06-05 04:01 pm (UTC) (Link)
`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?
 From: 2007-06-06 06:57 am (UTC) (Link)

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.
 From: 2007-06-08 06:15 am (UTC) (Link)
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.