Control.Eff.Logic

Logic primitives. See LogicT paper for details.

Documentation

class MSplit m where

The MSplit primitive from LogicT paper.

Methods

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

The laws for msplit are:

1] msplit mzero == return Nothing 2] msplit (return a mplus m) == return (Just(a, m))

Instances

Member NdetEff r => MSplit (Eff r)

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

Defined in Control.Eff.NdetEff

Methods

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

Member Choose r => MSplit (Eff r)

Defined in Control.Eff.Choose

Methods

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

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

Embed a pure value into MSplit

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

ifte :: (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: 1] ifte (return a) th el == th a 2] ifte mzero th el == el 3] ifte (return a mplus m) th el == th a mplus (m >>= th)

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

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

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

Negation as failure

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

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

1] interleave mzero m == m 2] 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

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

1] mzero >>- k == mzero 2] (return a mplus m) >>- k == interleave (k a) (m >>- k)

sols :: (MonadPlus 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.

TODO: use a more efficient data structure.