| 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 |
|---|---|
| License | BSD3 |
| Maintainer | Andrew Lelechenko <andrew.lelechenko@gmail.com> |
| Safe Haskell | Safe |
| Language | Haskell2010 |
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
- module Control.Monad.Logic.Class
- type Logic = LogicT Identity
- logic :: ( forall r. (a -> r -> r) -> r -> r) -> Logic a
- runLogic :: Logic a -> (a -> r -> r) -> r -> r
- observe :: Logic a -> a
- observeMany :: Int -> Logic a -> [a]
- 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 :: MonadFail m => LogicT m a -> m a
- observeManyT :: Monad m => Int -> LogicT m a -> m [a]
- observeAllT :: Applicative m => LogicT m a -> m [a]
- fromLogicT :: ( Alternative (t m), MonadTrans t, Monad m, Monad (t m)) => LogicT m a -> t m a
- fromLogicTWith :: ( Applicative m, Monad n, Alternative n) => ( forall x. m x -> n x) -> LogicT m a -> n a
- hoistLogicT :: ( Applicative m, Monad n) => ( forall x. m x -> n x) -> LogicT m a -> LogicT n a
- embedLogicT :: Applicative m => ( forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
Documentation
module Control.Monad.Logic.Class
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 [])
logic :: ( forall r. (a -> r -> r) -> r -> r) -> Logic a Source #
A smart constructor for
Logic
computations.
runLogic :: Logic a -> (a -> r -> r) -> r -> r Source #
Runs a
Logic
computation with the specified initial success and
failure continuations.
>>>runLogic empty (+) 00
>>>runLogic (pure 5 <|> pure 3 <|> empty) (+) 08
When invoked with
(:)
and
[]
as arguments, reveals
a half of the isomorphism between
Logic
and lists.
See description of
observeAll
for the other half.
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
.
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.
The LogicT monad transformer
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.
Instances
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
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.
observeManyT :: Monad m => Int -> LogicT m a -> m [a] Source #
Extracts up to a given number of results from a
LogicT
computation.
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.
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
fromLogicTWith :: ( Applicative m, Monad n, Alternative n) => ( forall x. m x -> n x) -> LogicT m a -> n a Source #
Convert from
to an arbitrary logic-like monad,
such as
LogicT
m
[]
.
Examples:
fromLogicT= fromLogicTWith dhoistLogicTf = fromLogicTWith (lift. f)embedLogicTf =fromLogicTWithf
The first argument should be a monad morphism . to produce sensible results.
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.
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.