9 views

Skip to first unread message

Dec 13, 2007, 12:59:20 AM12/13/07

to caml...@inria.fr

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu