Home

Polymorphic Delimited Continuations

Polymorphic Delimited Contiunations by Kenichi Asai and Yukiyoshi Kameyama, in the 5th ASIAN Symposium on Programming Languages and Systems (2007).

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

Now, the real reason that I post this is because of Oleg's ShiftResetGenuine, which implements polymorphic delimited continuations in Haskell, and primarily cites this paper as well as Robert Atkey's Parameterized Notions of Computation. So if you find this paper challenging to read, Oleg provides you with a concrete playground in which to experiment.

It's also notable that Matthieu Sozeau has GenuineShiftReset available, which is a Coq version of Oleg's code.

By Leon P Smith at 2009-04-23 04:16 | Functional | other blogs | 7550 reads

Comment viewing options

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

From Shift and Reset to Polarized Linear Logic

It's worth mentioning that I found Chung-chieh Shan's paper From Shift and Reset to Polarized Linear Logic to be immensely helpful in conjunction with Oleg's code. The first three sections give an algorithm for deriving direct-style expressions that map onto arbitrary expressions when passed through the CPS transform.

Also, people who are familiar with monads should not get too intimidated by Oleg's code: as pointed out by Dan Piponi's blog post Beyond Monads, you can simply treat Monadish as a regular monad, and use GHC's type inference algorithm to see what happens to your favorite examples. In fact, this provides you with one kind of type and effect system, although I'm unclear on the details.

By Leon P Smith at Thu, 2009-04-23 04:24 | login or register to post comments