Module `Choice`

Backtracking monad

Example

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

Then, running

run_n 1 (bogosort [2;3;5;1;0]);;

yields

- : int list list = [[0; 1; 2; 3; 5]]

type 'a t: A choice among values of type 'a

type 'a choice = 'a t

Combinators

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

yields

- : int list = [30; 27; 24; 21; 18; 15; 12; 9; 6; 3]

val delay : (unit -> 'a t) -> 'a t: 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

since: 0.4

val cons : 'a -> 'a t -> 'a t: cons x c is a shortcut for return x ++ c

val mplus : 'a t -> 'a t -> 'a t: mplus a b enumerates choices from a, then choices from b.

val bind : ('a -> 'b t) -> 'a t -> 'b t: Monadic bind. Each solution of the first argument is given to the function, that may in turn return several choices.

val interleave : 'a t -> 'a t -> 'a t: Same as mplus, but fair, ie it enumerates solutions alternatively from its first and second arguments.

val fair_bind : ('a -> 'b t) -> 'a t -> 'b t: Fair version of bind.

val ite : 'a t -> ('a -> 'b t) -> 'b t -> 'b t: ite cond th el enumerates the choices of cond. If cond fails, then it behaves like el, otherwise each solution of cond is given to th.

val map : ('a -> 'b) -> 'a t -> 'b t: Map solutions to other solutions

val product : 'a t -> 'b t -> ('a * 'b) t: Cartesian product of two choices

val fmap : ('a -> 'b option) -> 'a t -> 'b t: Special case of bind, with only zero or one possible output choices for each input choice.

val filter : ('a -> bool) -> 'a t -> 'a t: Only keep the solutions that satisfy the given predicate.

val once : 'a t -> 'a t: Retain at most one solution (drop alternatives).

val take : int -> 'a t -> 'a t: Retain at most n solutions

Enumerate solutions

val run_one : 'a t -> 'a option: Run until we get one answer (or a failure)

val run_n : int -> 'a t -> 'a list: The 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 to_seq : 'a t -> 'a Seq.t

Lazy iterator over the choices.

since: 0.4

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: return true iff the alternative stream is empty (failure)

val forall : bool t -> bool
val exists : bool t -> bool

Monadic operators

val lift : ('a -> 'b) -> 'a t -> 'b t
val lift2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val liftFair : ('a -> 'b) -> 'a t -> 'b t
val liftFair2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val pure : ('a -> 'b) -> ('a -> 'b) t
val app : ('a -> 'b) t -> 'a t -> 'b t: Applicative instance

val ($$) : ('a -> 'b) t -> 'a t -> 'b t: Shortcut for app

Infix operators

val (>>=) : 'a t -> ('a -> 'b t) -> 'b t: Infix version of bind

val (>>-) : 'a t -> ('a -> 'b t) -> 'b t: Infix version of fair_bind

val (++) : 'a t -> 'a t -> 'a t: Infix version of mplus

val (<|>) : 'a t -> 'a t -> 'a t: Infix version of interleave

Enumerator

module Enum : sig ... end

More complex Combinators

module List : sig ... end

module Array : sig ... end