[Haskell] Genuine shift/reset in Haskell98

[oleg at okmij.org]

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