#### choice 0.4 0.3 0.2 0.1

back to documentation root
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library choice
Module

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 guard : bool -> unit t`

Fails if condition does not hold

• since NEXT_RELEASE
`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`

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