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=1.1 required=5.0 tests=AWL,HTML_MESSAGE,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 25324BC69 for ; Wed, 3 Oct 2007 13:28:25 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGIZA0fAXQInemdsb2JhbACCPDWLRwIJCg X-IronPort-AV: E=Sophos;i="4.21,224,1188770400"; d="scan'208";a="2321445" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 03 Oct 2007 13:28:25 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l93BSNNw015767 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 3 Oct 2007 13:28:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGIZA0fRVZKxkmdsb2JhbACCPDWLRwIBAQcEBCc X-IronPort-AV: E=Sophos;i="4.21,224,1188770400"; d="scan'208";a="17234608" Received: from wa-out-1112.google.com ([209.85.146.177]) by mail4-smtp-sop.national.inria.fr with ESMTP; 03 Oct 2007 13:28:21 +0200 Received: by wa-out-1112.google.com with SMTP id m34so6188749wag for ; Wed, 03 Oct 2007 04:28:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:references; bh=nGl+M2+D7oL+gVXLviTL/lqxSIw0GfM9MvWgc7lPtcg=; b=i02VwKLwNIXgvmjShSdkgnhMMc5scLL0ycbbcRaBiTfWHQ5VgIEr/JXcbOZHqhWRx7DIQHRH61V6XDYAUayQYLGw39pGixXJNRmijdut9maOSKfVt6XmBhvyvMu58/MHC0luNgk93crkZ7cbIl465WsirTj0EJXGEJaZa1XrBkU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:references; b=n0WspvuNsTPFg6rXJj8SbHO2kqXzCBBNQmLJU789zN98i4iD1cY4t19b0i66p341dAfcjk2rVi+XkHkNB9BUffV/bQNpzhkMf0HRIAFn2wtgxxN6BOyWvB2C5lfm4yuV7Crwhfr+B2yX3XwDcj+Rw/ZoNHKWM8s+LQrtl2wAWHU= Received: by 10.114.132.5 with SMTP id f5mr3823836wad.1191410868430; Wed, 03 Oct 2007 04:27:48 -0700 (PDT) Received: by 10.114.25.8 with HTTP; Wed, 3 Oct 2007 04:27:48 -0700 (PDT) Message-ID: Date: Wed, 3 Oct 2007 13:27:48 +0200 From: kirillkh To: oleg@pobox.com Subject: Re: Locally-polymorphic exceptions [was: folding over a file] Cc: caml-list@inria.fr In-Reply-To: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_22978_29493760.1191410868426" References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> X-Miltered: at concorde with ID 47037CD8.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 delimited:01 oleg:01 unspecified:01 delimited:01 channel-:01 'a-:01 'b-:01 prev:01 val:01 prev:01 val:01 compiler:01 channel-:01 'a-:01 ------=_Part_22978_29493760.1191410868426 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Oleg, This looks excellent! I am especially delighted with the fact you don't have to declare this single-use exception in the global scope anymore. Could you be more specific regarding the continuations' performance impact? Would it matter in practice? Would you recommend using this function in a general-purpose library instead of the imperative-style implementation that was suggested? Also, is there a good manual on delimited continuations for a beginner with minimum of external references? I have tried to read your papers, but it's hard to advance because some of the complex stuff is explained elsewhere. -Kirill 2007/10/3, oleg@pobox.com : > > > kirillkh wrote > > Is there a way to instantiate an exception with a value of unspecified > type > > and then do explicit casting on catch? > > Surprisingly, the answer in many (or all?) cases is yes. The answer is > definitely yes in the case when we need to define an exception local > to a polymorphic function. Incidentally, SML permits declarations of > such local exceptions whose type is tied to that of the host > polymorphic function. That feature has been used to implement > delimited continuations. Perhaps unsurprisingly, delimited > continuations can be used to implement such locally-polymorphic > exceptions. > > The recent thread gave a good motivation for locally polymorphic > exceptions: writing a library function fold_file. The following code > has been proposed. > > > exception Done of 'a > > > > let fold_file (file: in_channel) > > (read_func: in_channel->'a) > > (elem_func: 'a->'b->'b) > > (seed: 'b) = > > let rec loop prev_val = > > let input = > > try read_func file > > with End_of_file -> raise (Done prev_val) > > in > > let combined_val = elem_func input prev_val in > > loop combined_val > > in > > try loop seed with Done x -> x > > Alas, the compiler does not accept the exception declaration, because > the declaration says that the exception should carry a value of all > types. There is no value that belongs to all types (and if it were, it > wouldn't be useful). But we don't actually need the value of all > types. We need the value of our Done exception to have the same type > as the result of the polymorphic function fold_file. We should have > declared the exception Done _inside_ fold_file. And that can be done: > Delimcc.prompt is precisely this type of `local exceptions'. > > So, we can implement fold_file, by slightly adjusting the above code: > > let fold_file (file: in_channel) > (read_func: in_channel->'a) > (elem_func: 'a->'b->'b) > (seed: 'b) = > let result = new_prompt () in (* here is our local exn declaration *) > let rec loop prev_val = > let input = > try read_func file > with End_of_file -> abort result prev_val > in > let combined_val = elem_func input prev_val in > loop combined_val > in > push_prompt result (fun () -> loop seed) > ;; > > (* > val fold_file : > in_channel -> (in_channel -> 'a) -> ('a -> 'b -> 'b) -> 'b -> 'b = > *) > > let line_count filename = > let f = open_in filename in > let counter _ count = count + 1 in > fold_file f input_line counter 0;; > > (* > val line_count : string -> int = > *) > > let test = line_count "/etc/motd";; > (* > val test : int = 24 > *) > > > The analogy between exceptions and delimited continuations is > profound: in fact, delimited continuations are implemented in terms of > exceptions. Abort is truly raise. Well, observationally. The current > delimcc library tried to follow Dybvig, Sabry and Peyton-Jones > interface -- which, being minimalistic, did not include abort as a > primitive. We have to implement abort in terms of take_subcont, which > is wasteful as we save the captured continuation for no good > reason. Internally, the library does have an abort primitive, and it > indeed works in the same way as raise. > > ------=_Part_22978_29493760.1191410868426 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Oleg,

This looks excellent! I am especially delighted with the fact you don't have to declare this single-use exception in the global scope anymore.
Could you be more specific regarding the continuations' performance impact? Would it matter in practice? Would you recommend using this function in a general-purpose library instead of the imperative-style implementation that was suggested?

Also, is there a good manual on delimited continuations for a beginner with minimum of external references? I have tried to read your papers, but it's hard to advance because some of the complex stuff is explained elsewhere.

-Kirill

2007/10/3, oleg@pobox.com <oleg@pobox.com>:

kirillkh wrote
> Is there a way to instantiate an exception with a value of unspecified type
> and then do explicit casting on catch?

Surprisingly, the answer in many (or all?) cases is yes. The answer is
definitely yes in the case when we need to define an exception local
to a polymorphic function. Incidentally, SML permits declarations of
such local exceptions whose type is tied to that of the host
polymorphic function. That feature has been used to implement
delimited continuations. Perhaps unsurprisingly, delimited
continuations can be used to implement such locally-polymorphic
exceptions.

The recent thread gave a good motivation for locally polymorphic
exceptions: writing a library function fold_file. The following code
has been proposed.

> exception Done of 'a
>
>  let fold_file (file: in_channel)
>               (read_func: in_channel->'a)
>               (elem_func: 'a->'b->'b)
>               (seed: 'b) =
>   let rec loop prev_val =
>     let input =
>       try read_func file
>       with End_of_file -> raise (Done prev_val)
>     in
>       let combined_val = elem_func input prev_val in
>       loop combined_val
>   in
>     try loop seed with Done x -> x

Alas, the compiler does not accept the exception declaration, because
the declaration says that the exception should carry a value of all
types. There is no value that belongs to all types (and if it were, it
wouldn't be useful). But we don't actually need the value of all
types. We need the value of our Done exception to have the same type
as the result of the polymorphic function fold_file. We should have
declared the exception Done _inside_ fold_file. And that can be done:
Delimcc.prompt is precisely this type of `local exceptions'.

So, we can implement fold_file, by slightly adjusting the above code:

let fold_file (file: in_channel)
              (read_func: in_channel->'a)
              (elem_func: 'a->'b->'b)
              (seed: 'b) =
  let result = new_prompt () in (* here is our local exn declaration *)
  let rec loop prev_val =
     let input =
       try read_func file
       with End_of_file -> abort result prev_val
     in
       let combined_val = elem_func input prev_val in
       loop combined_val
   in
     push_prompt result (fun () -> loop seed)
;;

(*
val fold_file :
  in_channel -> (in_channel -> 'a) -> ('a -> 'b -> 'b) -> 'b -> 'b = <fun>
*)

let line_count filename =
   let f = open_in filename in
   let counter _ count = count + 1 in
   fold_file f input_line counter 0;;

(*
val line_count : string -> int = <fun>
*)

let test = line_count "/etc/motd";;
(*
val test : int = 24
*)


The analogy between exceptions and delimited continuations is
profound: in fact, delimited continuations are implemented in terms of
exceptions. Abort is truly raise. Well, observationally. The current
delimcc library tried to follow Dybvig, Sabry and Peyton-Jones
interface -- which, being minimalistic, did not include abort as a
primitive. We have to implement abort in terms of take_subcont, which
is wasteful as we save the captured continuation for no good
reason. Internally, the library does have an abort primitive, and it
indeed works in the same way as raise.


------=_Part_22978_29493760.1191410868426--