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));;