From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=2.0 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id ED29EBC6B for ; Thu, 13 Dec 2007 06:58:53 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPJYYEfAXQImh2dsb2JhbACOeXQBAQEICik X-IronPort-AV: E=Sophos;i="4.24,160,1196636400"; d="scan'208";a="20263916" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Dec 2007 06:58:53 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id lBD5wqcY023746 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 13 Dec 2007 06:58:53 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah4FAC5ZYEfAEKcgYWdsb2JhbACOeWoVByw X-IronPort-AV: E=Sophos;i="4.24,160,1196636400"; d="scan'208";a="6756805" Received: from selenite.metnet.navy.mil ([192.16.167.32]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Dec 2007 06:58:51 +0100 Received: (qmail 21839 invoked by uid 107); 13 Dec 2007 05:58:50 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.152) by selenite.metnet.navy.mil with SMTP; 13 Dec 2007 05:58:50 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id A6AE5ACB7; Wed, 12 Dec 2007 21:56:43 -0800 (PST) From: oleg@okmij.org To: caml-list@inria.fr Subject: First-class typed, direct-style sprintf Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org Message-Id: <20071213055643.A6AE5ACB7@Adric.metnet.fnmoc.navy.mil> Date: Wed, 12 Dec 2007 21:56:43 -0800 (PST) X-Miltered: at discorde with ID 4760CA1C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 sprintf:01 sprintf:01 danvy:01 ocaml:01 printf:01 danvy:01 unparsing:01 compiler:01 unparsing:01 polymorphism:01 inference:01 haskell:01 monads:01 haskell:01 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 = 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 = 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 = 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 = # fmt int;; - : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt str;; - : (string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt int ^^ lit "xx";; - : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt int ^^ fmt str;; - : (int -> string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = 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.