Control.Eff.Logic.NDet

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.

Main interface

data NDet a

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

More performant handler; uses reified job queue

Defined in Control.Eff.Logic.NDet

Methods

handle :: (Eff r a -> [Eff r a] -> Eff r' (f w)) -> Arrs r v a -> NDet v -> [Eff r a] -> Eff r' (f w)

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)

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)

Alternative f => Handle NDet r a (Eff r' (f w))

Given a callback and NDet requests respond to them. Note that this makes explicit that we rely on f to have enough room to store all possibilities.

Defined in Control.Eff.Logic.NDet

Methods

handle :: (Eff r a -> Eff r' (f w)) -> Arrs r v a -> NDet v -> Eff r' (f w)

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)

respond_relay :: (a -> Eff r' (f w)) -> (Eff r a -> Eff r' (f w)) -> Eff r a -> Eff r' (f w)

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

Defined in Control.Eff.Logic.NDet

Associated Types

type StM (Eff (NDet ': r)) a :: Type

Methods

liftBaseWith :: (RunInBase (Eff (NDet ': r)) m -> m a) -> Eff (NDet ': r) a

restoreM :: StM (Eff (NDet ': r)) a -> Eff (NDet ': r) a

type StM (Eff (NDet ': r)) a

Defined in Control.Eff.Logic.NDet

type StM (Eff (NDet ': r)) a = StM (Eff r) [a]

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

How to embed a pure value in non-deterministic context

left :: Arrs r Bool a -> Eff r a

The left branch

right :: Arrs r Bool a -> Eff r a

The right branch

choose :: Member NDet r => [a] -> Eff r a

choose lst non-deterministically chooses one value from the lst. choose [] thus corresponds to failure.

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

Same as makeChoiceA, except it has the type hardcoded. Required for MonadBaseControl instance.

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

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

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

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

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

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

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

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

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

Methods

call :: MonadPlus (Eff r) => Eff (Exc CutFalse ': r) a -> Eff r a

Member NDet r => Alternative (Eff r)

Methods

empty :: Eff r a

(<|>) :: Eff r a -> Eff r a -> Eff r a

some :: Eff r a -> Eff r [a]

many :: Eff r a -> Eff r [a]

Member NDet r => MonadPlus (Eff r)

Mapping of NDet requests to MonadPlus. We obey the following laws (taken from the Backtr and @LogicT papers):

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

NOTE that we do not obey the right-zero law for mzero. Specifically, we do not obey:

m >> mzero  = mzero

Methods

mzero :: Eff r a

mplus :: Eff r a -> Eff r a -> Eff r a

Member NDet r => MSplit (Eff r)

We implement LogicT, the non-determinism reflection, of which soft-cut is one instance. See the LogicT paper for an explanation.

Methods

msplit :: Eff r a -> Eff r (Maybe (a, Eff r a))