Moduleextensible-effects-5.0.0.1Haskell2010

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.

1 type
10 values

Packageextensible-effects-5.0.0.1
Exports11
LanguageHaskell2010
LicenceMIT
SourceNDet.hs

Main interface

7 declarations

datadata NDet a where

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

Instances4Handle, MonadBaseControl, StM

Alternative f => Handle NDet r a (Eff r' (f w))Defined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet
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.
Alternative f => Handle NDet r a ([Eff r a] -> Eff r' (f w))Defined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet
More performant handler; uses reified job queue
(MonadBase m m, LiftedBase m r) => MonadBaseControl m (Eff (NDet ': r))Defined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet
type StM (Eff (NDet ': r)) a = StM (Eff r) [a]Defined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet

valuewithNDet :: (Alternative f, Monad m) => a -> m (f a)

How to embed a pure value in non-deterministic context

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

The left branch

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

The right branch

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

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

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

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

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

4 declarations

valuemsplit' :: 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.

valuemsplit'_manual :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a))

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

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

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

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

4 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
Member NDet r => Alternative (Eff r)

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

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.