Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

Nondeterministic choice effect via MPlus interface directly. In order to get an understanding of what nondeterministic choice entails the following papers are recommended:

- [
`LogicT`

] LogicT - backtracking monad transformer with fair operations and pruning - [
`Backtr`

] Deriving Backtracking Monad Transformers

**TODO**: investigate Fusion regd msplit and associated functions.

## Synopsis

- data NDet a
- withNDet :: Alternative f => Monad m => a -> m (f a)
- left :: Arrs r Bool a -> Eff r a
- right :: Arrs r Bool a -> Eff r a
- choose :: Member NDet r => [a] -> Eff r a
- makeChoice :: Eff (NDet ': r) a -> Eff r [a]
- makeChoiceA :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)
- module Control.Eff.Logic.Core
- msplit' :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a))
- msplit'_manual :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a))
- makeChoiceA_manual :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)
- makeChoiceA0 :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)

# Main interface

An implementation of non-deterministic choice aka backtracking. The two
requests we need to support are: `false`

, `(|)`

. We map this to the
`MonadPlus`

(or `Alternative`

) interface: `MZero`

stands for `false`

, and
`MPlus`

stands for `(|)`

.

This creates a branching structure with a fanout of `2`

, resulting in `mplus`

node being visited approximately `2x`

(in general, for a fanout of `f`

we'll
have the type of internal node being invoked `f/(f-1)`

times).

## Instances

Alternative f => Handle NDet r a ([Eff r a] -> Eff r' (f w)) Source # | More performant handler; uses reified job queue |

Defined in Control.Eff.Logic.NDet handle :: (Eff r a -> [Eff r a] -> Eff r' (f w)) -> Arrs r v a -> NDet v -> [Eff r a] -> Eff r' (f w) Source # handle_relay :: (r ~ (NDet ': r'0), Relay ([Eff r a] -> Eff r' (f w)) r'0) => (a -> [Eff r a] -> Eff r' (f w)) -> (Eff r a -> [Eff r a] -> Eff r' (f w)) -> Eff r a -> [Eff r a] -> Eff r' (f w) Source # respond_relay :: (a -> [Eff r a] -> Eff r' (f w)) -> (Eff r a -> [Eff r a] -> Eff r' (f w)) -> Eff r a -> [Eff r a] -> Eff r' (f w) Source # | |

Alternative f => Handle NDet r a (Eff r' (f w)) Source # | Given a callback and |

Defined in Control.Eff.Logic.NDet handle :: (Eff r a -> Eff r' (f w)) -> Arrs r v a -> NDet v -> Eff r' (f w) Source # handle_relay :: (r ~ (NDet ': r'0), Relay (Eff r' (f w)) r'0) => (a -> Eff r' (f w)) -> (Eff r a -> Eff r' (f w)) -> Eff r a -> Eff r' (f w) Source # respond_relay :: (a -> Eff r' (f w)) -> (Eff r a -> Eff r' (f w)) -> Eff r a -> Eff r' (f w) Source # | |

(MonadBase m m, LiftedBase m r) => MonadBaseControl m (Eff (NDet ': r)) Source # | |

type StM (Eff (NDet ': r)) a Source # | |

withNDet :: Alternative f => Monad m => a -> m (f a) Source #

How to embed a pure value in non-deterministic context

makeChoice :: Eff (NDet ': r) a -> Eff r [a] Source #

Same as `makeChoiceA`

, except it has the type hardcoded.
Required for `MonadBaseControl`

instance.

makeChoiceA :: Alternative f => Eff (NDet ': r) a -> Eff r (f a) Source #

Optimized implementation, faster and taking less memory. The benefit of the effect framework is that we can have many interpreters.

module Control.Eff.Logic.Core

# Additional functions for comparison

msplit' :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a)) Source #

The implementation of `MSplit`

. Exported as a standalone to make
testing/comparison easier.

msplit'_manual :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a)) Source #

A different implementation, more involved, but similar complexity to
`msplit'`

.

makeChoiceA_manual :: Alternative f => Eff (NDet ': r) a -> Eff r (f a) Source #

A different implementation, more involved, but similar complexity to
`makeChoiceA`

.

makeChoiceA0 :: Alternative f => Eff (NDet ': r) a -> Eff r (f a) Source #

An interpreter: The following is very simple, but leaks a lot of memory The
cause probably is mapping every failure to empty It takes then a lot of timne
and space to store those empty. When there aren't a lot of failures, this is
comparable to `makeChoiceA`

.

# Orphan instances

Member NDet r => Call r Source # | The call interpreter -- it is like reify . reflect with a twist. Compare this implementation with the huge implementation of call in Hinze 2000 (Figure 9). Each clause corresponds to the axiom of call or cutfalse. All axioms are covered. The code clearly expresses the intuition that call watches the choice points of its argument computation. When it encounteres a cutfalse request, it discards the remaining choicepoints. It completely handles CutFalse effects but not non-determinism |

Member NDet r => Alternative (Eff r) Source # | |

Member NDet r => MonadPlus (Eff r) Source # | Mapping of mzero >>= f = mzero -- (L1) mzero `mplus` m = m -- (L2) m `mplus` mzero = m -- (L3) m `mplus` (n `mplus` o) = (m `mplus` n) `mplus` o -- (L4) (m `mplus` n) >>= k = (m >>= k) `mplus` (n >>= k) -- (L5) `L1` is the left-zero law for`mzero` `L2, L3, L4` are the`Monoid` laws
m >> mzero = mzero |

Member NDet r => MSplit (Eff r) Source # | We implement LogicT, the non-determinism reflection, of which soft-cut is one instance. See the LogicT paper for an explanation. |