Moduleextensible-effects-5.0.0.1Haskell2010

Control.Eff.Logic.Core

Logic primitives. See LogicT paper for details.

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

1 type
2 classes
11 values

Packageextensible-effects-5.0.0.1
Exports14
LanguageHaskell2010
LicenceMIT
SourceCore.hs

classclass MSplit (m :: Type -> Type) where

The MSplit primitive from LogicT paper.

Methods

msplit :: m a -> m (Maybe (a, m a))

The laws for msplit are:

msplit mzero                = return Nothing
msplit (return a `mplus` m) = return (Just(a, m))

Instances1MSplit

Member NDet r => MSplit (Eff r)Defined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet · orphan
We implement LogicT, the non-determinism reflection, of which soft-cut is one instance. See the LogicT paper for an explanation.

valuewithMSplit :: MonadPlus m => a -> m a -> m (Maybe (a, m a))

Embed a pure value into MSplit

valuereflect :: MonadPlus m => Maybe (a, m a) -> m a

Laws for reflect:

msplit (lift m >> mzero)   >>= reflect = lift m >> mzero
msplit (lift m `mplus` ma) >>= reflect = lift m `mplus` (msplit ma >>= reflect)

valueifte :: (MonadPlus m, MSplit m) => m t -> (t -> m b) -> m b -> m b

Soft-cut: non-deterministic if-then-else, aka Prolog's *-> Declaratively,

 ifte t th el = (t >>= th) `mplus` ((not t) >> el)

However, t is evaluated only once. In other words, ifte t th el is equivalent to t >>= th if t has at least one solution. If t fails, ifte t th el is the same as el. Laws:

ifte (return a) th el           = th a
ifte mzero th el                = el
ifte (return a `mplus` m) th el = th a `mplus` (m >>= th)

valueonce :: (MSplit m, MonadPlus m) => m b -> m b

Another pruning operation (ifte is the other). This selects one solution out of possibly many.

valuegnot :: (MonadPlus m, MSplit m) => m b -> m ()

Negation as failure

valueinterleave :: (MSplit m, MonadPlus m) => m b -> m b -> m b

Fair (i.e., avoids starvation) disjunction. It obeys the following laws:

interleave mzero m                  = m
interleave (return a `mplus` m1) m2 = return a `mplus` (interleave m2 m1)

corollary:

interleave m mzero = m

value(>>-) :: (MonadPlus m, MSplit m) => m a -> (a -> m b) -> m b

Fair (i.e., avoids starvation) conjunction. It obeys the following laws:

mzero                >>- k = mzero
(return a `mplus` m) >>- k = interleave (k a) (m >>- k)

valuesols :: (Monad m, MSplit m) => m a -> m [a]

Collect all solutions. This is from Hinze's Backtr monad class. Unsurprisingly, this can be implemented in terms of msplit.

classclass Call (r :: [Type -> Type]) where

Non-determinism with control (cut).

For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper:

[Backtr] Deriving Backtracking Monad Transformers

Hinze suggests expressing cut in terms of cutfalse:

= return () `mplus` cutfalse
where
 cutfalse :: m a

satisfies the following laws:

 cutfalse >>= k  = cutfalse              (F1)
 cutfalse | m    = cutfalse              (F2)

(note: m `mplus` cutfalse is different from cutfalse `mplus` m). In other words, cutfalse is the left zero of both bind and mplus.

Hinze also introduces the operation call :: m a -> m a that delimits the effect of cut: call m executes m. If the cut is invoked in m, it discards only the choices made since m was called. Hinze postulates the axioms of call:

 call false = false                          (C1)
 call (return a | m) = return a | call m     (C2)
 call (m | cutfalse) = call m                (C3)
 call (lift m >>= k) = lift m >>= (call . k) (C4)

call m behaves like m except any cut inside m has only a local effect, he says.

Hinze noted a problem with the "mechanical" derivation of backtracing monad transformer with cut: no axiom specifying the interaction of call with bind; no way to simplify nested invocations of call.

Methods

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

Mapping Backtr interface to MonadPlus and using exceptions for cutfalse, every instance should ensure that the following laws hold:

 cutfalse `mplus` m        = cutfalse                --(F2)
 call mzero                = mzero                   --(C1)
 call (return a `mplus` m) = return a `mplus` call m --(C2)
 call (m `mplus` cutfalse) = call m                  --(C3)
 call (lift m >>= k)       = lift m >>= (call . k)   --(C4)

Instances2Call

Member NDet r => Call rDefined in extensible-effects-5.0.0.1 · Control.Eff.Logic.NDet · orphan
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
(MonadPlus (Eff (Exc CutFalse ': r)), MSplit (Eff (Exc CutFalse ': r))) => Call rDefined in extensible-effects-5.0.0.1 · Control.Eff.Logic.Experimental · orphan

datadata CutFalse

CutFalse

valuecutfalse :: Member (Exc CutFalse) r => Eff r a

We use exceptions for cutfalse Therefore, the law cutfalse >>= k = cutfalse is satisfied automatically since all exceptions have the above property.

value(!) :: (Member (Exc CutFalse) r, MonadPlus (Eff r)) => Eff r ()

Prolog cut, taken from Hinze 2000 (Deriving backtracking monad transformers).

valuelist :: b -> (a -> [a] -> b) -> [a] -> b

Case analysis for lists