logict-0.8.1.0: A backtracking logic-programming monad.
Copyright(c) 2007-2014 Dan Doel
(c) 2011-2013 Edward Kmett
(c) 2014 Roman Cheplyaka
(c) 2020-2021 Andrew Lelechenko
(c) 2020-2021 Kevin Quick
LicenseBSD3
MaintainerAndrew Lelechenko <andrew.lelechenko@gmail.com>
Safe HaskellSafe
LanguageHaskell2010

Control.Monad.Logic

Description

Adapted from the paper Backtracking, Interleaving, and Terminating Monad Transformers by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry. Note that the paper uses MonadPlus vocabulary (mzero and mplus), while examples below prefer empty and <|> from Alternative.

Synopsis

Documentation

The Logic monad

type Logic = LogicT Identity Source #

The basic Logic monad, for performing backtracking computations returning values (e.g. Logic a will return values of type a).

Technical perspective. Logic is a Boehm-Berarducci encoding of lists. Speaking plainly, its type is identical (up to Identity wrappers) to foldr applied to a given list. And this list itself can be reconstructed by supplying (:) and [].

import Data.Functor.Identity

fromList :: [a] -> Logic a
fromList xs = LogicT $ \cons nil -> foldr cons nil xs

toList :: Logic a -> [a]
toList (LogicT fld) = runIdentity $ fld (\x (Identity xs) -> Identity (x : xs)) (Identity [])

Here is a systematic derivation of the isomorphism. We start with observing that [a] is isomorphic to a fix point of a non-recursive base algebra Fix (ListF a):

newtype Fix f = Fix (f (Fix f))
data ListF a r = ConsF a r | NilF deriving (Functor)

cata :: Functor f => (f r -> r) -> Fix f -> r
cata f = go where go (Fix x) = f (fmap go x)

from :: [a] -> Fix (ListF a)
from = foldr (\a acc -> Fix (ConsF a acc)) (Fix NilF)

to :: Fix (ListF a) -> [a]
to = cata (\case ConsF a r -> a : r; NilF -> [])

Further, Fix (ListF a) is isomorphic to Boehm-Berarducci encoding ListC a:

newtype ListC a = ListC (forall r. (ListF a r -> r) -> r)

from :: Fix (ListF a) -> ListC a
from xs = ListC (\f -> cata f xs)

to :: ListC a -> Fix (ListF a)
to (ListC f) = f Fix

Finally, ListF a rr is isomorphic to a pair (arr, r), so ListC is isomorphic to the Logic type modulo Identity wrappers:

newtype Logic a = Logic (forall r. (a -> r -> r) -> r -> r)

And wrapping every occurence of r into m gives us LogicT:

newtype LogicT m a = Logic (forall r. (a -> m r -> m r) -> m r -> m r)

Since: 0.5.0

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

A smart constructor for Logic computations.

Since: 0.5.0

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

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

>>> runLogic empty (+) 0
0
>>> runLogic (pure 5 <|> pure 3 <|> empty) (+) 0
8

When invoked with (:) and [] as arguments, reveals a half of the isomorphism between Logic and lists. See description of observeAll for the other half.

Since: 0.2

observe :: Logic a -> a Source #

Extracts the first result from a Logic computation, failing if there are no results.

>>> observe (pure 5 <|> pure 3 <|> empty)
5
>>> observe empty
*** Exception: No answer.

Since Logic is isomorphic to a list, observe is analogous to head.

Since: 0.2

observeMany :: Int -> Logic a -> [a] Source #

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

>>> let nats = pure 0 <|> fmap (+ 1) nats
>>> observeMany 5 nats
[0,1,2,3,4]

Since Logic is isomorphic to a list, observeMany is analogous to take.

Since: 0.2

observeAll :: Logic a -> [a] Source #

Extracts all results from a Logic computation.

>>> observeAll (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)
[5,3]

observeAll reveals a half of the isomorphism between Logic and lists. See description of runLogic for the other half.

Since: 0.2

The LogicT monad transformer

newtype LogicT m a Source #

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

When m is Identity, LogicT m becomes isomorphic to a list (see Logic). Thus LogicT m for non-trivial m can be imagined as a list, pattern matching on which causes monadic effects.

Since: 0.2

Constructors

LogicT 

Fields

  • unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r
     

Instances

Instances details
MonadTrans LogicT Source # 
Instance details

Defined in Control.Monad.Logic

Methods

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

MonadError e m => MonadError e (LogicT m) Source #

Since: 0.4

Instance details

Defined in Control.Monad.Logic

Methods

throwError :: e -> LogicT m a #

catchError :: LogicT m a -> (e -> LogicT m a) -> LogicT m a #

MonadReader r m => MonadReader r (LogicT m) Source # 
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) Source # 
Instance details

Defined in Control.Monad.Logic

Methods

get :: LogicT m s #

put :: s -> LogicT m () #

state :: (s -> (a, s)) -> LogicT m a #

MonadFail (LogicT m) Source #

Since: 0.6.0.3

Instance details

Defined in Control.Monad.Logic

Methods

fail :: String -> LogicT m a #

MonadIO m => MonadIO (LogicT m) Source # 
Instance details

Defined in Control.Monad.Logic

Methods

liftIO :: IO a -> LogicT m a #

MonadZip m => MonadZip (LogicT m) Source #

Since: 0.8.0.0

Instance details

Defined in Control.Monad.Logic

Methods

mzip :: LogicT m a -> LogicT m b -> LogicT m (a, b) #

mzipWith :: (a -> b -> c) -> LogicT m a -> LogicT m b -> LogicT m c #

munzip :: LogicT m (a, b) -> (LogicT m a, LogicT m b) #

Foldable (LogicT Identity) Source #

Since: 0.5.0

Instance details

Defined in Control.Monad.Logic

Methods

fold :: Monoid m => LogicT Identity m -> m #

foldMap :: Monoid m => (a -> m) -> LogicT Identity a -> m #

foldMap' :: Monoid m => (a -> m) -> LogicT Identity a -> m #

foldr :: (a -> b -> b) -> b -> LogicT Identity a -> b #

foldr' :: (a -> b -> b) -> b -> LogicT Identity a -> b #

foldl :: (b -> a -> b) -> b -> LogicT Identity a -> b #

foldl' :: (b -> a -> b) -> b -> LogicT Identity a -> b #

foldr1 :: (a -> a -> a) -> LogicT Identity a -> a #

foldl1 :: (a -> a -> a) -> LogicT Identity a -> a #

toList :: LogicT Identity a -> [a] #

null :: LogicT Identity a -> Bool #

length :: LogicT Identity a -> Int #

elem :: Eq a => a -> LogicT Identity a -> Bool #

maximum :: Ord a => LogicT Identity a -> a #

minimum :: Ord a => LogicT Identity a -> a #

sum :: Num a => LogicT Identity a -> a #

product :: Num a => LogicT Identity a -> a #

(Applicative m, Foldable m) => Foldable (LogicT m) Source #

Since: 0.5.0

Instance details

Defined in Control.Monad.Logic

Methods

fold :: Monoid m0 => LogicT m m0 -> m0 #

foldMap :: Monoid m0 => (a -> m0) -> LogicT m a -> 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) Source #

Since: 0.5.0

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

(Monad m, Traversable m) => Traversable (LogicT m) Source #

Since: 0.8.0.0

Instance details

Defined in Control.Monad.Logic

Methods

traverse :: Applicative f => (a -> f b) -> LogicT m a -> f (LogicT m b) #

sequenceA :: Applicative f => LogicT m (f a) -> f (LogicT m a) #

mapM :: Monad m0 => (a -> m0 b) -> LogicT m a -> m0 (LogicT m b) #

sequence :: Monad m0 => LogicT m (m0 a) -> m0 (LogicT m a) #

Alternative (LogicT f) Source # 
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] #

Applicative (LogicT f) Source # 
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 #

Functor (LogicT f) Source # 
Instance details

Defined in Control.Monad.Logic

Methods

fmap :: (a -> b) -> LogicT f a -> LogicT f b #

(<$) :: a -> LogicT f b -> LogicT f a #

Monad (LogicT m) Source # 
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 #

MonadPlus (LogicT m) Source # 
Instance details

Defined in Control.Monad.Logic

Methods

mzero :: LogicT m a #

mplus :: LogicT m a -> LogicT m a -> LogicT m a #

Monad m => MonadLogic (LogicT m) Source # 
Instance details

Defined in Control.Monad.Logic

Methods

msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a)) Source #

interleave :: LogicT m a -> LogicT m a -> LogicT m a Source #

(>>-) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b Source #

once :: LogicT m a -> LogicT m a Source #

lnot :: LogicT m a -> LogicT m () Source #

ifte :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b Source #

Monoid (LogicT m a) Source #

Since: 0.7.0.3

Instance details

Defined in Control.Monad.Logic

Methods

mempty :: LogicT m a #

mappend :: LogicT m a -> LogicT m a -> LogicT m a #

mconcat :: [LogicT m a] -> LogicT m a #

Semigroup (LogicT m a) Source #

Since: 0.7.0.3

Instance details

Defined in Control.Monad.Logic

Methods

(<>) :: LogicT m a -> LogicT m a -> LogicT m a #

sconcat :: NonEmpty (LogicT m a) -> LogicT m a #

stimes :: Integral b => b -> LogicT m a -> LogicT m a #

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

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

The second argument ("success continuation") takes one result of the LogicT computation and the monad to run for any subsequent matches.

The third argument ("failure continuation") is called when the LogicT cannot produce any more results.

For example:

>>> yieldWords = foldr ((<|>) . pure) empty
>>> showEach wrd nxt = putStrLn wrd >> nxt
>>> runLogicT (yieldWords ["foo", "bar"]) showEach (putStrLn "none!")
foo
bar
none!
>>> runLogicT (yieldWords []) showEach (putStrLn "none!")
none!
>>> showFirst wrd _ = putStrLn wrd
>>> runLogicT (yieldWords ["foo", "bar"]) showFirst (putStrLn "none!")
foo

Since: 0.2

observeT :: MonadFail m => LogicT m a -> m a Source #

Extracts the first result from a LogicT computation, failing if there are no results at all.

Since: 0.2

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

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

Since: 0.2

observeAllT :: Applicative m => LogicT m a -> m [a] Source #

Extracts all results from a LogicT computation, unless blocked by the underlying monad.

For example, given

>>> let nats = pure 0 <|> fmap (+ 1) nats

some monads (like Identity, Reader, Writer, and State) will be productive:

>>> take 5 $ runIdentity (observeAllT nats)
[0,1,2,3,4]

but others (like ExceptT, and ContT) will not:

>>> take 20 <$> runExcept (observeAllT nats)

In general, if the underlying monad manages control flow then observeAllT may be unproductive under infinite branching, and observeManyT should be used instead.

Since: 0.2

fromLogicT :: (Alternative (t m), MonadTrans t, Monad m, Monad (t m)) => LogicT m a -> t m a Source #

Convert from LogicT to an arbitrary logic-like monad transformer, such as list-t or logict-sequence

For example, to show a representation of the structure of a LogicT computation, l, over a data-like Monad (such as [], Data.Sequence.Seq, etc.), you could write

import ListT (ListT)

show $ fromLogicT @ListT l

Since: 0.8.0.0

fromLogicTWith :: (Applicative m, Monad n, Alternative n) => (forall x. m x -> n x) -> LogicT m a -> n a Source #

Convert from LogicT m to an arbitrary logic-like monad, such as [].

Examples:

fromLogicT = fromLogicTWith d
hoistLogicT f = fromLogicTWith (lift . f)
embedLogicT f = fromLogicTWith f

The first argument should be a monad morphism. to produce sensible results.

Since: 0.8.0.0

hoistLogicT :: (Applicative m, Monad n) => (forall x. m x -> n x) -> LogicT m a -> LogicT n a Source #

Convert a LogicT computation from one underlying monad to another. For example,

hoistLogicT lift :: LogicT m a -> LogicT (StateT m) a

The first argument should be a monad morphism. to produce sensible results.

Since: 0.8.0.0

embedLogicT :: Applicative m => (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b Source #

Convert a LogicT computation from one underlying monad to another.

The first argument should be a monad morphism. to produce sensible results.

Since: 0.8.0.0