[Caml-list] First-class typed, direct-style sprintf

[ol...@okmij.org]

We demonstrate direct-style typed sprintf: sprintf format_spec 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. Our sprintf and format specifiers are ordinary,
first-class functions, and so can be passed as arguments or returned
as results. The format specifiers can also be composed incrementally.
Unlike Danvy/Filinski's sprintf, the types seem to be simpler.

Recently there has been discussion contrasting the OCaml Printf module
with Danvy/Filinski's functional unparsing. The latter can be
implemented as a pure library function, requiring no special support
from the compiler. It does require writing the format specifiers in
the continuation-passing style, which makes types huge and
errors very difficult to find. Perhaps less known that
Danvy/Filinski's functional unparsing has a direct-style
counter-part. It is particularly elegant and simple: the whole
implementation takes only four lines of code. The various
implementations of typed sprintf are lucidly and insightfully
described in
http://pllab.is.ocha.ac.jp/~asai/papers/tr07-1.ps.gz

Alas, the elegant sprintf requires control operators supporting both
answer-type modification and polymorphism. The corresponding calculus
has been presented in the recent APLAS 2007 paper by Asai and
Kameyama. 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

At that time, only prototype implementation was available, in a
private version of mini-ML. Yesterday, a straightforward Haskell98
implementation of the calculus emerged, based on parameterized monads:
http://www.haskell.org/pipermail/haskell/2007-December/020034.html
It includes sprintf.

OCaml already has delimited control operators, in the delimcc
library. Those operators, too, support polymorphism. They are
different however, supporting multiple typed prompts, but the fixed
answer type (which is the type of the prompt). It has not been known
until today if the quantity of the prompts can make up for their
quality: can multi-prompt shift/reset (or, cupto) _emulate_ the
modification of the answer-type. We now know that the answer is yes.
Many elegant applications of shift/reset become possible; in
particular, `shift (fun k -> k)' becomes typeable. The latter has many
applications, e.g., in web form programming and linguistics.

The full implementation and many tests (of sprintf) are available at
http://okmij.org/ftp/ML/sprintf-cupto.ml

The following are a few notable excerpts. First are the definitions of
answer-type modifying, polymorphic shift/reset. Unlike the
fixed-answer-type shift/reset, which have one prompt, shift2/reset2
have two prompts, for the two answer types (before and after the
modification).

let reset2 f =
let p1 = new_prompt () in
let p2 = new_prompt () in
push_prompt p1 (fun () -> abort p2 (f (p1,p2)));;
val reset2 : ('a Delimcc.prompt * 'b Delimcc.prompt -> 'b) -> 'a = <fun>

let shift2 (p1,p2) f =
shift p1 (fun k -> fun x ->
push_prompt p2 (fun () -> f k x; failwith "omega"));;
val shift2 :
('a -> 'b) Delimcc.prompt * 'b Delimcc.prompt ->
(('c -> 'a -> 'b) -> 'a -> 'd) -> 'c = <fun>

At first sight, these definitions seem trivial. At the second sight,
they seem outright wrong, as 'abort p2' seem to be executed before the
corresponding prompt p2 is pushed. Hopefully, the fifth sight will
show that the definitions are indeed simple and do what they are
supposed to.

We can write the following append function (Sec 2.1 of Asai and
Kameyama's APLAS paper)

let rec append lst prompts =
match lst with
| [] -> shift2 prompts (fun k l -> k l)
| a::rest -> a :: append rest prompts;;

whose inferred type
'a list -> ('a list -> 'b) Delimcc.prompt * 'b Delimcc.prompt -> 'a list
clearly shows both the polymorphism (in 'b) and the answer-type
modification from 'b to 'a list -> 'b.

Here's the typed sprintf:

let test3 = sprintf (lit "The value of " ^^ fmt str ^^ lit " is " ^^ fmt int);;
val test3 : string -> int -> string = <fun>
let test3r = test3 "x" 1;;
val test3r : string = "The value of x is 1"

We can write this test in the following way, to demonstrate that
sprint and format specifiers are first-class and that the format
specification can be composed incrementally.

let test3' =
let format_spec1 = lit "The value of " ^^ fmt str ^^ lit " is " in
let format_spec = format_spec1 ^^ fmt int in
let applyit f x = f x in
let formatter = applyit sprintf format_spec in
formatter "x" 1;;

Here are the (inferred) types of format specifiers and of their compositions:

# lit "xx";;
- : '_a Delimcc.prompt * '_a Delimcc.prompt -> string = <fun>

# fmt int;;
- : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = <fun>
# fmt str;;
- : (string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = <fun>

# fmt int ^^ lit "xx";;
- : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = <fun>

# fmt int ^^ fmt str;;
- : (int -> string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string =<fun>

The type of (fmt int ^^ fmt str) clearly shows the answer-type
modification. One can read this as follows: given prompts, the
expression computes a string upon the hypotheses 'int' and 'string' in
that order.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs