From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oleg@okmij.org>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: *
X-Spam-Status: No, score=1.4 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38])
	by yquem.inria.fr (Postfix) with ESMTP id 9BBE5BC69
	for <caml-list@yquem.inria.fr>; Sat, 10 Feb 2007 12:17:27 +0100 (CET)
Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l1ABHOmv007702
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL)
	for <caml-list@inria.fr>; Sat, 10 Feb 2007 12:17:26 +0100
Received: (qmail 12064 invoked by uid 107); 10 Feb 2007 11:17:23 -0000
Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.102)
  by selenite.metnet.navy.mil with SMTP; 10 Feb 2007 11:17:23 -0000
Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760)
	id 3436EAB40; Sat, 10 Feb 2007 03:15:56 -0800 (PST)
To: Andrej.Bauer@andrej.com, jtbryant@valdosta.edu
Cc: caml-list@inria.fr
Subject: Amb
Reply-To: oleg@pobox.com
Errors-To: oleg@okmij.org
From: oleg@pobox.com
Message-Id: <20070210111556.3436EAB40@Adric.metnet.fnmoc.navy.mil>
Date: Sat, 10 Feb 2007 03:15:56 -0800 (PST)
X-Miltered: at discorde with ID 45CDA9C4.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; oleg:01 andrej:01 ocaml:01 delimited:01 toplevel:01 function':01 threading:01 delimited:01 sandbox:01 oleg:01 failwith:01 printf:01 printf:01 toplevel:01 invokes:01 


Andrej Bauer wrote:
> let me point out that amb is supposed to work as an _angelic_
> nondeterministic choice operator. This means it must choose a value
> that, if at all possible, leads to successful completion of the
> computation.... The scheme implementation involves callcc magic. 
> If anyone knows a reasonable implementation of amb, I'd be
> interested to know.

Here it is. Ocaml has something better than call/cc: delimited
continuations. So, amb is trivially implementable, in two lines of
code. We also need a `toplevel function', to tell us if the overall
computation succeeded. One may think of it as St.Peter at the
gate. For now, we take a computation that raises no exception as
successful. In general, even non-termination within a branch can be
dealt with intelligently (cf. `cooperative' threading which must yield
from time to time).

Regarding effects incurred while evaluating branches: one deal with
them as one deal with effects when implementing any transactional
mechanism: you prohibit them, you log the updates, you log the state
before the beginning so to undo, you use zipper for functional
`mutations' (which can be done with delimited continuations, too), you
operate in a sandbox, etc. The ZFS talk gives an example:
 http://pobox.com/~oleg/ftp/Computation/Continuations.html#zipper-fs

Here are the tests. The second one requires a three-step clairvoyance:

let test1 () =
  let v = 
    if (amb [(fun _ -> false); (fun _ -> true)]) then
      7
    else failwith "Sinner!"
  in Printf.printf "got the result %d\n" v;;
let test1r = toplevel test1;;
(* got the result 7 *)

(* Test that invokes the Pythagorean spirit *)
let numbers = List.map (fun n -> (fun () -> n)) [1;2;3;4;5];;
let pyth () = 
  let (v1,v2,v3) =
    let i = amb numbers in
    let j = amb numbers in
    let k = amb numbers in
    if i*i + j*j = k*k then (i,j,k) else failwith "too bad"
  in Printf.printf "got the result (%d,%d,%d)\n" v1 v2 v3;;

let pythr = toplevel pyth;;
(* got the result (3,4,5) *)

(* Open the DelimCC library
  http://pobox.com/~oleg/ftp/Computation/Continuations.html#caml-shift
*)
open Delimcc;;
let shift p f = take_subcont p (fun sk () ->
  push_prompt p (fun () -> (f (fun c -> 
    push_prompt p (fun () -> push_subcont sk c)))))
;;

(* How evaluation has finished *)
type res = 
    Done                             (* Finished with the result *)
  | Exc     of exn                   (* Got an exception -- no good *)
  | Choices of (unit -> res) list    (* Alternative universes *)

exception Amb		             (* Raise when all choices are bad *)
;;

let topprompt = new_prompt ();;

(* If it looks like an OS scheduler, it's because it is *)
let toplevel thunk =
  let rec loop queue = function 
  | Done (* evaluation of a branch finished successfully *)
     -> ()
  | Exc _ -> try_another queue
  | Choices more  -> (* OK, add them to the end: breadth-first *)
      try_another (queue @ more)
  and try_another = function
  |  [] -> raise Amb (* No more choices *)
  |  h::t -> loop t (try h () with e -> Exc e)
  in
  loop [] (push_prompt topprompt 
	     (fun () -> try let _ = thunk () in Done with e -> Exc e))
;;

(* Split the universe. Something like `fork (2)' *)
let amb choices = shift topprompt (fun sk -> 
  Choices (List.map (fun choice -> (fun () -> sk choice)) choices));;