select.eff

(* This example is described in Section 6.8 of "Programming with Algebraic Effects and
   Handlers" by A. Bauer and M. Pretnar. *)

(* A version of ambivalent choice which tells how it found the desired value. *)

type 'a result = Failure | Success of 'a

(* Select_int takes a variable name and a list of possible integer choices
   and chooses one. *)

effect Select_int: string * int list -> int

(* The handler tries out all choices until it finds one that leads to the
   desired outcome. All current choices are saved in an association list. *)

let selection_collector desired_outcome = handler
  | effect (Select_int (name, choices)) k -> (fun selected ->
    (* Check association list if variable already chosen. *)
    (match assoc name selected with
     | Some y -> (k y) selected
     | None ->
       (* Select a value and try to get desired outcome. *)
         let rec try_choice = function
           | [] -> Failure
           | y::ys ->
               (match (k y) ((name,y)::selected) with
                  | Success lst -> Success lst
                  | Failure -> try_choice ys)
         in try_choice choices))
  | outcome -> (fun selected ->
    (* Check if outcome is the desired one. *)
    if outcome = desired_outcome then Success selected else Failure)
  (* Because we are passing a state, we need to start with an empty assoc list.*)
  | finally f -> f []
;;

(* Search for a Pythagorean triple. It finds a=5, b=12, c=13. *)
with selection_collector true handle
  let a = perform (Select_int ("a", [5;6;7;8])) in
  let b = perform (Select_int ("b", [9;10;11;12])) in
  let c = perform (Select_int ("c", [13;14;15;16])) in
    a*a + b*b = c*c;;

(* Martin Escardo's epsilon. *)

effect Select_bool: int * bool list -> bool

(* Modify handler for booleans.*)
let selection_collector desired_outcome = handler
  | effect (Select_bool (name, choices)) k -> (fun selected ->
    (match assoc name selected with
     | Some y -> (k y) selected
     | None ->
         let rec try_choice = function
           | [] -> Failure
           | y::ys ->
               (match (k y) ((name,y)::selected) with
                  | Success lst -> Success lst
                  | Failure -> try_choice ys)
         in try_choice choices))
  | outcome -> (fun selected ->
    if outcome = desired_outcome then Success selected else Failure)
  | finally f -> f [];;

(* Define epsilon. *)
let epsilon p =
    let r = (with selection_collector true handle
               p (fun n -> perform (Select_bool (n, [false; true]))))
    in
      match r with
        | Failure -> (fun _ -> false)
        | Success lst ->
          (fun n -> match assoc n lst with
                    | None -> false | Some b -> b)
  ;;

(* From epsilon we can define existential and universal quantifiers. *)
let some p = p (epsilon p);;
let every p = not (p (epsilon (fun x -> not (p x))));;

(* And equality on the Cantor space. *)
let equal x y = every (fun k -> x k = y k);;

(* A sample predicate. *)
let p x = (if x (10 ** 1000) then x (2 ** 30000) else not (x (3 ** 40000)));;

some p;; (* true, answer found instantaneously *)

(* xor n x takes the exclusive or of x 0, x 1, ..., x n. *)
let rec xor n x =
  if n = 0 then x 0 else x n <> xor (n-1) x;;

(* It is not much more difficult to get a witness for xor. *)
take (epsilon (xor 300)) 300;;

(* To get an example which takes some time we need a predicate
   which is true only on a small portion of the entire space. *)
let rec is_alternating n b x =
  if n = 0 then x 0 = b else
    let u = (x n = b) in
    let v = is_alternating (n-1) (not b) x in
      u && v;;

take (epsilon (is_alternating 15 true)) 20;;