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.