Sunday, May 2, 2010

Polarity and the logic of delimited continuations

Text: pdf
Code: twelf

Polarized logic is the logic of values and continuations, and their interaction through continuation-passing style. The main limitations of this logic are the limitations of CPS: that continuations cannot be composed, and that programs are fully sequentialized. Delimited control operators were invented in response to the limitations of classical continuation-passing. That suggests the question: what is the logic of delimited continuations?

We offer a simple account of delimited control, through a natural generalization of the classical notion of polarity. This amounts to breaking the perfect symmetry between positive and negative polarity in the following way: answer types are positive. Despite this asymmetry, we retain all of the classical polarized connectives, and can explain "intuitionistic polarity" (e.g., in systems like CBPV) as a restriction on the use of connectives, i.e., as a logical fragment. Our analysis complements and generalizes existing accounts of delimited control operators, while giving us a rich logical language through which to understand the interaction of control with monadic effects.

To appear at LICS 2010.

Writing this paper helped me sort out some things I'd been puzzled about for a while—I hope you also find it useful!


Neel Krishnaswami said...

This is lovely, Noam!

You have finally given me a reason to care about delimited continuations, and it is a really good one. Dare I hope you are preparing a paper on "Nomics" next? :-)

Noam said...

Thanks Neel!

Nomics, you mean like this? Actually that's an intriguing idea to relate to game semantics... :)

Neel Krishnaswami said...

I was actually thinking of "intuitionistic ludics", with delimited continuations playing a similar role as full continuations do in ludics. I dubbed this hypothetical theory 'Nomics' as a play on your name and ludics. :)

More seriously, not-not-closure is an idea that has just kept on winning year after year, in every area of semantics. I actually don't know how old it is; I've seen variants of this idea as far back as the mid-1980s (in denotational semantics), with people writing as if it is a well-known technique.

Since it's such a powerful technique, any improvement to it is a really exciting prospect.

Neel Krishnaswami said...

I have a question, Noam. I just read Hugo Herbelin's paper on Markov's principle, and I noticed that he has "call/cc for positive types", which is similar to the restriction on delimited continuations you use.

Obviously, this can't be a coincidence! But I don't even know what questions I should be asking about this similarity. Can you tell me what the questions to ask are?

Noam said...

Yeah we've thought about that (note Hugo's office is 10m away from mine!). I think the question to ask (which I asked in my paper) might be as simple as, what do you get by combining delimited continuations with the exceptions monad? In particular that seems to be what Oleg Kiselyov is doing in this post on
Constructive Law of Excluded Middle
. It would be nice (and Hugo and his student Danko Ilik are also thinking about this) to relate these approaches to Kripke semantics for Markov's principle, such as Coquand and Hofmann's.