Safe Haskell	Safe
Language	Haskell2010

Logic

Contents

Logic
LogicT
MonadLogic

Synopsis

type Logic = LogicT Identity
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
runLogic :: Logic a -> (a -> r -> r) -> r -> r
observeAll :: Logic a -> [a]
newtype LogicT (m :: * -> *) a = LogicT {
- unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r
}
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
observeT :: Monad m => LogicT m a -> m a
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeAllT :: Monad m => LogicT m a -> m [a]
class MonadPlus m => MonadLogic (m :: * -> *)
msplit :: MonadLogic m => m a -> m (Maybe (a, m a))
interleave :: MonadLogic m => m a -> m a -> m a
(>>-) :: MonadLogic m => m a -> (a -> m b) -> m b
ifte :: MonadLogic m => m a -> (a -> m b) -> m b -> m b
once :: MonadLogic m => m a -> m a
reflect :: MonadLogic m => Maybe (a, m a) -> m a
lnot :: MonadLogic m => m a -> m ()

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
Fields unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r

Instances

MonadTrans LogicT
Instance details Defined in Control.Monad.Logic Methods lift :: Monad m => m a -> LogicT m a #
MonadReader r m => MonadReader r (LogicT m)
Instance details Defined in Control.Monad.Logic Methods ask :: LogicT m r # local :: (r -> r) -> LogicT m a -> LogicT m a # reader :: (r -> a) -> LogicT m a #
MonadState s m => MonadState s (LogicT m)
Instance details Defined in Control.Monad.Logic Methods get :: LogicT m s # put :: s -> LogicT m () # state :: (s -> (a, s)) -> LogicT m a #
MonadError e m => MonadError e (LogicT m)
Instance details Defined in Control.Monad.Logic Methods throwError :: e -> LogicT m a # catchError :: LogicT m a -> (e -> LogicT m a) -> LogicT m a #
Monad (LogicT m)
Instance details Defined in Control.Monad.Logic Methods (>>=) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b # (>>) :: LogicT m a -> LogicT m b -> LogicT m b # return :: a -> LogicT m a # fail :: String -> LogicT m a #
Functor (LogicT f)
Instance details Defined in Control.Monad.Logic Methods fmap :: (a -> b) -> LogicT f a -> LogicT f b # (<$) :: a -> LogicT f b -> LogicT f a #
Applicative (LogicT f)
Instance details Defined in Control.Monad.Logic Methods pure :: a -> LogicT f a # (<>) :: LogicT f (a -> b) -> LogicT f a -> LogicT f b # liftA2 :: (a -> b -> c) -> LogicT f a -> LogicT f b -> LogicT f c # (>) :: LogicT f a -> LogicT f b -> LogicT f b # (<*) :: LogicT f a -> LogicT f b -> LogicT f a #
(Monad m, Foldable m) => Foldable (LogicT m)
Instance details Defined in Control.Monad.Logic Methods fold :: Monoid m0 => LogicT m m0 -> m0 # foldMap :: Monoid m0 => (a -> m0) -> LogicT m a -> m0 # foldr :: (a -> b -> b) -> b -> LogicT m a -> b # foldr' :: (a -> b -> b) -> b -> LogicT m a -> b # foldl :: (b -> a -> b) -> b -> LogicT m a -> b # foldl' :: (b -> a -> b) -> b -> LogicT m a -> b # foldr1 :: (a -> a -> a) -> LogicT m a -> a # foldl1 :: (a -> a -> a) -> LogicT m a -> a # toList :: LogicT m a -> [a] # null :: LogicT m a -> Bool # length :: LogicT m a -> Int # elem :: Eq a => a -> LogicT m a -> Bool # maximum :: Ord a => LogicT m a -> a # minimum :: Ord a => LogicT m a -> a # sum :: Num a => LogicT m a -> a # product :: Num a => LogicT m a -> a #
Traversable (LogicT Identity)
Instance details Defined in Control.Monad.Logic Methods traverse :: Applicative f => (a -> f b) -> LogicT Identity a -> f (LogicT Identity b) # sequenceA :: Applicative f => LogicT Identity (f a) -> f (LogicT Identity a) # mapM :: Monad m => (a -> m b) -> LogicT Identity a -> m (LogicT Identity b) # sequence :: Monad m => LogicT Identity (m a) -> m (LogicT Identity a) #
Alternative (LogicT f)
Instance details Defined in Control.Monad.Logic Methods empty :: LogicT f a # (<\|>) :: LogicT f a -> LogicT f a -> LogicT f a # some :: LogicT f a -> LogicT f [a] # many :: LogicT f a -> LogicT f [a] #
MonadPlus (LogicT m)
Instance details Defined in Control.Monad.Logic Methods mzero :: LogicT m a # mplus :: LogicT m a -> LogicT m a -> LogicT m a #
MonadIO m => MonadIO (LogicT m)
Instance details Defined in Control.Monad.Logic Methods liftIO :: IO a -> LogicT m a #
Monad m => MonadLogic (LogicT m)
Instance details Defined in Control.Monad.Logic Methods msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a)) # interleave :: LogicT m a -> LogicT m a -> LogicT m a # (>>-) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b # ifte :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b # once :: LogicT m a -> LogicT m a #

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.

MonadLogic

class MonadPlus m => MonadLogic (m :: * -> *) #

Minimal implementation: msplit

Minimal complete definition

msplit

Instances

MonadLogic []
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: [a] -> [Maybe (a, [a])] # interleave :: [a] -> [a] -> [a] # (>>-) :: [a] -> (a -> [b]) -> [b] # ifte :: [a] -> (a -> [b]) -> [b] -> [b] # once :: [a] -> [a] #
Monad m => MonadLogic (LogicT m)
Instance details Defined in Control.Monad.Logic Methods msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a)) # interleave :: LogicT m a -> LogicT m a -> LogicT m a # (>>-) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b # ifte :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b # once :: LogicT m a -> LogicT m a #
(MonadLogic m, Monoid w) => MonadLogic (WriterT w m)
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: WriterT w m a -> WriterT w m (Maybe (a, WriterT w m a)) # interleave :: WriterT w m a -> WriterT w m a -> WriterT w m a # (>>-) :: WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b # ifte :: WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b -> WriterT w m b # once :: WriterT w m a -> WriterT w m a #
MonadLogic m => MonadLogic (StateT s m)
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a)) # interleave :: StateT s m a -> StateT s m a -> StateT s m a # (>>-) :: StateT s m a -> (a -> StateT s m b) -> StateT s m b # ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b # once :: StateT s m a -> StateT s m a #
MonadLogic m => MonadLogic (StateT s m)
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a)) # interleave :: StateT s m a -> StateT s m a -> StateT s m a # (>>-) :: StateT s m a -> (a -> StateT s m b) -> StateT s m b # ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b # once :: StateT s m a -> StateT s m a #
(MonadLogic m, Monoid w) => MonadLogic (WriterT w m)
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: WriterT w m a -> WriterT w m (Maybe (a, WriterT w m a)) # interleave :: WriterT w m a -> WriterT w m a -> WriterT w m a # (>>-) :: WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b # ifte :: WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b -> WriterT w m b # once :: WriterT w m a -> WriterT w m a #
MonadLogic m => MonadLogic (ReaderT e m)
Instance details Defined in Control.Monad.Logic.Class Methods msplit :: ReaderT e m a -> ReaderT e m (Maybe (a, ReaderT e m a)) # interleave :: ReaderT e m a -> ReaderT e m a -> ReaderT e m a # (>>-) :: ReaderT e m a -> (a -> ReaderT e m b) -> ReaderT e m b # ifte :: ReaderT e m a -> (a -> ReaderT e m b) -> ReaderT e m b -> ReaderT e m b # once :: ReaderT e m a -> ReaderT e m a #

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