This message announces the Haskell98 implementation of Asai and Kameyama's polymorphic delimited continuations, with effect typing, full soundness (well-typed terms don't give any run-time exceptions), answer-type modification and polymorphism. Thanks to parameterized monads the implementation is the straightforward translation of the rules of the calculus. Parameterized monads seem to have proven their claim for syntactic sugar. http://okmij.org/ftp/Haskell/ShiftResetGenuine.hs Delimited control operators shift/reset are, fortunately, becoming popular. Alas, all widely available implementations suffer deficiencies: for example, the type system does not prevent attempts to execute shift outside the dynamic scope of reset, which leads to a run-time error. Furthermore, the implementations do not permit modifications of the answer-type, and so make impossible many elegant applications of shift/reset such as fully typed sprintf. In particular, shift id (or, shift return, in the monadic form), so often used in linguistics, are not typeable in any widely available implementation of delimited continuations. Related to the first issue, implemented calculi of delimited continuations are not strongly normalizing. That fact has been known for some time; it has been shown recently that the calculus of multi-prompt delimited continuations -- the DC calculus of the DDBinding paper, implemented in the DelimCC Haskell library -- expresses the fix-point combinator and emulates general recursive types, and so is, in fact, Turing complete. http://okmij.org/ftp/Computation/Continuations.html#delimcc-rectype Back in 1989 Danvy and Filinski recognized that ensuring strong type soundness (aka, control decency: no naked shift) requires a type-and-effect system. They proposed a (monomorphically typed) type system with answer-type modifications. Alas, it has not been implemented in any widely available language (or even formally published for that matter: the only source is the DIKU Technical Report). In the recent APLAS 2007 paper, Asai and Kameyama have developed a polymorphically typed calculus of delimited continuations with answer type modifications. They have proven greatly desirable properties of their calculus: strong type soundness, principal types, the existence of a type inference algorithm, preservation of types and equality through CPS translation, confluence, strong normalization for the subcalculus without fix. http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf http://pllab.is.ocha.ac.jp/~asai/papers/aplas07slide.pdf The particularly elegant application of their calculus is typed sprintf: sprintf format_expression arg1 arg2 .... The type system ensures that the number and the types of format specifiers in format_expression agree with the number and the types of arg1, etc. Provided control operators supporting both answer-type modification and polymorphism, sprintf is expressible as a regular function (and a very simple one: the entire solution takes only four lines). This problem is described in more detail in http://pllab.is.ocha.ac.jp/~asai/papers/tr07-1.ps.gz Alas, Asai and Kameyama's calculus has only been implemented in a privately modified version of mini-ML. This link at the beginning points to the complete, short implementation, including the sprintf example. The implementation is in Haskell98; contrary to the popular belief, the latter is still a capable language. Thus the genuine control operators have become practically available for the first time. We rely on parameterized monads, Robert Atkey, Parameterised Notions of Computation, Msfp2006 http://homepages.inf.ed.ac.uk/ratkey/param-notions.pdf see also http://www.haskell.org/pipermail/haskell/2006-December/018917.html To be more precise, we represent the the effectful expression e, whose type is characterized by the judgment Gamma; a |- e:tau; b as a parameterized monad C a b tau. We represent an effectful function type sigma/a -> tau/b of the calculus as an arrow type sigma -> C a b tau. We greatly benefit from two lucky circumstances. First, the rule 'app' of Asai and Kameyama (Fig 3 of their paper) turns out to be expressible as a composition of two binds in the parameterized monad. Second, the existing type inference of Haskell matches unbelievably well with the let-rule of Asai and Kameyama: the type of only pure expressions can be generalized. Indeed, impure expressions have the type C a b tau and can be meaningfully used only with bind, which forces the monomorphic treatment. Pure expressions such as functions, numbers, etc. can be applied without the assistance of bind; luckily, Haskell generalizes the type in their definitions automatically. The rest of the implementation is the trivial transcription of the types in Fig 3 and the derivation of the corresponding proof terms. The sprintf test has the following form (slightly less elegant compared to ML) stest1 = run $ sprintf (ret "Hello world") -- "Hello world" stest2 = run $ sprintf (ret "Hello " ^ fmt str ^ ret "!") $$ "world" -- "Hello world!" stest3 = run $ sprintf (ret "The value of " ^ fmt str ^ ret " is " ^ fmt int) $$ "x" $$ 3 -- "The value of x is 3" Obviously, the type of sprintf (format_expression) depends on the number and the type of format specifiers (fmt) in the format expression. The function sprintf is a simple ordinary function: sprintf p = reset p