planet-mitchell-0.1.0: Planet Mitchell

Logic

Contents

Synopsis

## Logic

type Logic = LogicT Identity #

The basic Logic monad, for performing backtracking computations returning values of type a

logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a #

A smart constructor for Logic computations.

runLogic :: Logic a -> (a -> r -> r) -> r -> r #

Runs a Logic computation with the specified initial success and failure continuations.

observeAll :: Logic a -> [a] #

Extracts all results from a Logic computation.

## LogicT

newtype LogicT (m :: * -> *) a #

A monad transformer for performing backtracking computations layered over another monad m

Constructors

 LogicT FieldsunLogicT :: forall r. (a -> m r -> m r) -> m r -> m r
Instances

runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r #

Runs a LogicT computation with the specified initial success and failure continuations.

observeT :: Monad m => LogicT m a -> m a #

Extracts the first result from a LogicT computation, failing otherwise.

observeManyT :: Monad m => Int -> LogicT m a -> m [a] #

Extracts up to a given number of results from a LogicT computation.

observeAllT :: Monad m => LogicT m a -> m [a] #

Extracts all results from a LogicT computation.

Minimal implementation: msplit

Minimal complete definition

msplit

Instances

msplit :: MonadLogic m => m a -> m (Maybe (a, m a)) #

Attempts to split the computation, giving access to the first result. Satisfies the following laws:

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

interleave :: MonadLogic m => m a -> m a -> m a #

Fair disjunction. It is possible for a logical computation to have an infinite number of potential results, for instance:

odds = return 1 mplus liftM (2+) odds

Such computations can cause problems in some circumstances. Consider:

do x <- odds mplus return 2
if even x then return x else mzero

Such a computation may never consider the 'return 2', and will therefore never terminate. By contrast, interleave ensures fair consideration of both branches of a disjunction

(>>-) :: MonadLogic m => m a -> (a -> m b) -> m b infixl 1 #

Fair conjunction. Similarly to the previous function, consider the distributivity law for MonadPlus:

(mplus a b) >>= k = (a >>= k) mplus (b >>= k)

If 'a >>= k' can backtrack arbitrarily many tmes, (b >>= k) may never be considered. (>>-) takes similar care to consider both branches of a disjunctive computation.

ifte :: MonadLogic m => m a -> (a -> m b) -> m b -> m b #

Logical conditional. The equivalent of Prolog's soft-cut. If its first argument succeeds at all, then the results will be fed into the success branch. Otherwise, the failure branch is taken. satisfies the following 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 :: MonadLogic m => m a -> m a #

Pruning. Selects one result out of many. Useful for when multiple results of a computation will be equivalent, or should be treated as such.

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

The inverse of msplit. Satisfies the following law:

msplit m >>= reflect == m

lnot :: MonadLogic m => m a -> m () #

Inverts a logic computation. If m succeeds with at least one value, lnot m fails. If m fails, then lnot m succeeds the value ().