Module Choice

module Choice: sig .. end

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 Choice.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 Choice.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 Choice.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 : 'a t -> int
Number of solutions
val is_empty : 'a 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 Choice.app

Infix operators


val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
Infix version of Choice.bind
val (>>-) : 'a t -> ('a -> 'b t) -> 'b t
Infix version of Choice.fair_bind
val (++) : 'a t -> 'a t -> 'a t
Infix version of Choice.mplus
val (<|>) : 'a t -> 'a t -> 'a t
Infix version of Choice.interleave

Enumerator


module Enum: sig .. end

More complex Combinators


module List: sig .. end
module Array: sig .. end