Some design choices are slightly different, since OCaml is strict. Performance may also vary from ghc-compiled code, since it performs some optimizations like deforestation.
We adapt the example from the LogicT paper.
let rec insert e l = match l with |  -> return [e] | x::l' -> mplus (return (e :: l)) (insert e l' >>= fun l'' -> return (x :: l''));; let rec permute = function |  -> return  | x::l -> permute l >>= fun l' -> insert x l';; let rec sorted l = match l with |  | [_] -> true | x::((y::l') as l) -> x <= y && sorted l;; let bogosort l = once (filter sorted (permute l));;
run_n 1 (bogosort [2;3;5;1;0]);;
- : int list list = [[0; 1; 2; 3; 5]]
type 'a choice = 'a t
val return : 'a -> 'a t
Return a value, and succeed
val of_list : 'a list -> 'a t
Multiple returns. Each element of the list is a candidate for success.
val from_fun : ( unit -> 'a option ) -> 'a t
Call the function to get alternative choices. Example:
let r = ref 0 in Choice.run_n 10 (Choice.filter (Choice.from_fun (fun () -> incr r; Some !r)) (fun x -> x mod 3 = 0));;
- : int list = [30; 27; 24; 21; 18; 15; 12; 9; 6; 3]
Delay the computation (the closure will be called in each branch that uses the choice point
val fail : 'a t
Fail to yield a solution.
val guard : bool -> unit t
Fails if condition does not hold
Monadic bind. Each solution of the first argument is given to the function, that may in turn return several choices.
mplus, but fair, ie it enumerates solutions alternatively from its first and second arguments.
ite cond th el enumerates the choices of
cond fails, then it behaves like
el, otherwise each solution of
cond is given to
Special case of
bind, with only zero or one possible output choices for each input choice.
Only keep the solutions that satisfy the given predicate.
val run_one : 'a t -> 'a option
Run until we get one answer (or a failure)
val run_n : int -> 'a t -> 'a list
n first solutions, in reverse order.
val run_all : 'a t -> 'a list
All the solutions (in reverse order)
val to_list : 'a t -> 'a list
All the solutions (in correct order)
val iter : 'a t -> ( 'a -> bool ) -> unit
Enumerate solutions, until none remains, or the callback returns
false to signal it has had enough solutions
val fold : ( 'a -> 'b -> 'a ) -> 'a -> 'b t -> 'a
Fold over all solutions
val count : _ t -> int
Number of solutions
val is_empty : _ t -> bool
true iff the alternative stream is empty (failure)
val forall : bool t -> bool
val exists : bool t -> bool
val pure : ( 'a -> 'b ) -> ( 'a -> 'b ) t
module Enum : sig ... end
module List : sig ... end
module Array : sig ... end