On Typing Delimited Continuations:
Three New Solutions to the Printf Problem
In ``Functional Unparsing'' (JFP 8(6):621-625, 1998),
Danvy presented a type-safe printf function using continuations and an
accumulator to achieve the effect of dependent types.
The key technique employed in Danvy's solution is the non-standard use
of continuations: not all of its calls are tail calls, i.e., it uses
delimited continuations.
Against this backdrop, we present three new solutions to the
printf problem: a simpler one that also uses delimited continuations
but that does not use an accumulator, and the corresponding two in
direct style with the delimited-control operators,
shift and reset.
These two solutions are the direct-style counterparts of the two
continuation-based ones.
The last solution pinpoints the essence of Danvy's solution:
shift is used to
change the answer type of delimited continuations.
Besides providing a new
application of
shift and reset,
the solutions in direct style raise a
key issue in the typing of first-class delimited continuations and
require Danvy and Filinski's original type system.
The resulting types precisely account for the behavior of printf.
This is the extended version of the previous technical report
OCHA-IS 07-1.
It contains an introduction to continuation-passing style and
delimited-control operators, shift and reset.