Module `Choice`

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

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

package choice

Module Choice