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

Language | Haskell2010 |

Logic primitives. See `LogicT`

paper for details.

## Synopsis

- class MSplit m where
- withMSplit :: MonadPlus m => a -> m a -> m (Maybe (a, m a))
- reflect :: MonadPlus m => Maybe (a, m a) -> m a
- ifte :: (MonadPlus m, MSplit m) => m t -> (t -> m b) -> m b -> m b
- once :: (MSplit m, MonadPlus m) => m b -> m b
- gnot :: (MonadPlus m, MSplit m) => m b -> m ()
- interleave :: (MSplit m, MonadPlus m) => m b -> m b -> m b
- (>>-) :: (MonadPlus m, MSplit m) => m a -> (a -> m b) -> m b
- sols :: (Monad m, MSplit m) => m a -> m [a]
- class Call r where
- data CutFalse = CutFalse
- cutfalse :: Member (Exc CutFalse) r => Eff r a
- (!) :: (Member (Exc CutFalse) r, MonadPlus (Eff r)) => Eff r ()
- list :: b -> (a -> [a] -> b) -> [a] -> b

# Documentation

The MSplit primitive from LogicT paper.

withMSplit :: MonadPlus m => a -> m a -> m (Maybe (a, m a)) Source #

Embed a pure value into MSplit

reflect :: MonadPlus m => Maybe (a, m a) -> m a Source #

Laws for `reflect`

:

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

ifte :: (MonadPlus m, MSplit m) => m t -> (t -> m b) -> m b -> m b Source #

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)

once :: (MSplit m, MonadPlus m) => m b -> m b Source #

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

interleave :: (MSplit m, MonadPlus m) => m b -> m b -> m b Source #

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

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

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

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

sols :: (Monad m, MSplit m) => m a -> m [a] Source #

Collect all solutions. This is from Hinze's `Backtr`

monad
class. Unsurprisingly, this can be implemented in terms of msplit.

Non-determinism with control (`cut`

).

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

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

is different from `mplus`

` cutfalse`cutfalse ``

).
In other words, cutfalse is the left zero of both bind and mplus.`mplus`

` m

Hinze also introduces the operation

that
delimits the effect of cut: `call`

:: m a -> m a

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`

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

behaves like `call`

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

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

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)

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

(MonadPlus (Eff ((Exc CutFalse :: Type -> Type) ': r)), MSplit (Eff ((Exc CutFalse :: Type -> Type) ': r))) => Call r Source # | |

cutfalse :: Member (Exc CutFalse) r => Eff r a Source #

We use exceptions for cutfalse
Therefore, the law `cutfalse >>= k = cutfalse`

is satisfied automatically since all exceptions have the above property.