Module `Choice`Source

Backtracking monad

This is an attempt to implement the Logic monad, as described in this Haskell library or in this paper.

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.

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]]

Sourcetype 'a t

A choice among values of type 'a

Sourcetype 'a choice = 'a t

Combinators

Sourceval return : 'a -> 'a t

Return a value, and succeed

Sourceval of_list : 'a list -> 'a t

Multiple returns. Each element of the list is a candidate for success.

Sourceval 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]

Sourceval delay : (unit -> 'a t) -> 'a t

Delay the computation (the closure will be called in each branch that uses the choice point

Sourceval fail : 'a t

Fail to yield a solution.

Sourceval guard : bool -> unit t

Fails if condition does not hold

since 0.4

Sourceval cons : 'a -> 'a t -> 'a t

cons x c is a shortcut for return x ++ c

Sourceval mplus : 'a t -> 'a t -> 'a t

mplus a b enumerates choices from a, then choices from b.

Sourceval 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.

Sourceval interleave : 'a t -> 'a t -> 'a t

Same as mplus, but fair, ie it enumerates solutions alternatively from its first and second arguments.

Sourceval fair_bind : ('a -> 'b t) -> 'a t -> 'b t

Fair version of bind.

Sourceval 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.

Sourceval map : ('a -> 'b) -> 'a t -> 'b t

Map solutions to other solutions

Sourceval product : 'a t -> 'b t -> ('a * 'b) t

Cartesian product of two choices

Sourceval fmap : ('a -> 'b option) -> 'a t -> 'b t

Special case of bind, with only zero or one possible output choices for each input choice.

Sourceval filter : ('a -> bool) -> 'a t -> 'a t

Only keep the solutions that satisfy the given predicate.

Sourceval once : 'a t -> 'a t

Retain at most one solution (drop alternatives).

Sourceval take : int -> 'a t -> 'a t

Retain at most n solutions

Enumerate solutions

Sourceval run_one : 'a t -> 'a option

Run until we get one answer (or a failure)

Sourceval run_n : int -> 'a t -> 'a list

The n first solutions, in reverse order.

Sourceval run_all : 'a t -> 'a list

All the solutions (in reverse order)

Sourceval to_list : 'a t -> 'a list

All the solutions (in correct order)

Sourceval iter : 'a t -> ('a -> bool) -> unit

Enumerate solutions, until none remains, or the callback returns false to signal it has had enough solutions

Sourceval to_seq : 'a t -> 'a Seq.t

Lazy iterator over the choices.

since 0.4

Sourceval fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a

Fold over all solutions

Sourceval count : _ t -> int

Number of solutions

Sourceval is_empty : _ t -> bool

return true iff the alternative stream is empty (failure)

Sourceval forall : bool t -> bool

Sourceval exists : bool t -> bool

Monadic operators

Sourceval lift : ('a -> 'b) -> 'a t -> 'b t

Sourceval lift2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t

Sourceval liftFair : ('a -> 'b) -> 'a t -> 'b t

Sourceval liftFair2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t

Sourceval pure : ('a -> 'b) -> ('a -> 'b) t

Sourceval app : ('a -> 'b) t -> 'a t -> 'b t

Applicative instance

Sourceval ($$) : ('a -> 'b) t -> 'a t -> 'b t

Shortcut for app

Infix operators

Sourceval (>>=) : 'a t -> ('a -> 'b t) -> 'b t

Infix version of bind

Sourceval (>>-) : 'a t -> ('a -> 'b t) -> 'b t

Infix version of fair_bind

Sourceval (++) : 'a t -> 'a t -> 'a t

Infix version of mplus

Sourceval (<|>) : 'a t -> 'a t -> 'a t

Infix version of interleave

Enumerator

Sourcemodule Enum : sig ... end

More complex Combinators

Sourcemodule List : sig ... end

Sourcemodule Array : sig ... end

package choice

Module ChoiceSource