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.