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
License | BSD3
Maintainer | Andrew Lelechenko <andrew.lelechenko@gmail.com>
Safe Haskell | Safe
Language | Haskell2010

Control.Monad.Logic

Contents

- The Logic monad
- The LogicT monad transformer

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 [])

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` `r` → `r` is isomorphic to a pair (`a` → `r` → `r`, `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 Source #
MonadError e m => MonadError e (LogicT m) Source # | Since: 0.4
Instance details Defined in Control.Monad.Logic Methods throwError :: e -> LogicT m a Source # catchError :: LogicT m a -> (e -> LogicT m a) -> LogicT m a Source #
MonadReader r m => MonadReader r (LogicT m) Source # |
Instance details Defined in Control.Monad.Logic Methods ask :: LogicT m r Source # local :: (r -> r) -> LogicT m a -> LogicT m a Source # reader :: (r -> a) -> LogicT m a Source #
MonadState s m => MonadState s (LogicT m) Source # |
Instance details Defined in Control.Monad.Logic Methods get :: LogicT m s Source # put :: s -> LogicT m () Source # state :: (s -> (a, s)) -> LogicT m a Source #
MonadFail (LogicT m) Source # | Since: 0.6.0.3
Instance details Defined in Control.Monad.Logic Methods fail :: String -> LogicT m a Source #
MonadIO m => MonadIO (LogicT m) Source # |
Instance details Defined in Control.Monad.Logic Methods liftIO :: IO a -> LogicT m a Source #
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) Source # mzipWith :: (a -> b -> c) -> LogicT m a -> LogicT m b -> LogicT m c Source # munzip :: LogicT m (a, b) -> (LogicT m a, LogicT m b) Source #
Foldable (LogicT Identity) Source # | Since: 0.5.0

Instance details

Defined in Control.Monad.Logic

Methods

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

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

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

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

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

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

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

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

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

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

null :: LogicT Identity a -> Bool Source #

length :: LogicT Identity a -> Int Source #

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

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

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

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

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

(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 Source #

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

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

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

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

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

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

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

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

toList :: LogicT m a -> [a] Source #

null :: LogicT m a -> Bool Source #

length :: LogicT m a -> Int Source #

elem :: Eq a => a -> LogicT m a -> Bool Source #

maximum :: Ord a => LogicT m a -> a Source #

minimum :: Ord a => LogicT m a -> a Source #

sum :: Num a => LogicT m a -> a Source #

product :: Num a => LogicT m a -> a Source #

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) Source # sequenceA :: Applicative f => LogicT Identity (f a) -> f (LogicT Identity a) Source # mapM :: Monad m => (a -> m b) -> LogicT Identity a -> m (LogicT Identity b) Source # sequence :: Monad m => LogicT Identity (m a) -> m (LogicT Identity a) Source #
(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) Source # sequenceA :: Applicative f => LogicT m (f a) -> f (LogicT m a) Source # mapM :: Monad m0 => (a -> m0 b) -> LogicT m a -> m0 (LogicT m b) Source # sequence :: Monad m0 => LogicT m (m0 a) -> m0 (LogicT m a) Source #
Alternative (LogicT f) Source # |
Instance details Defined in Control.Monad.Logic Methods empty :: LogicT f a Source # (<|>) :: LogicT f a -> LogicT f a -> LogicT f a Source # some :: LogicT f a -> LogicT f [a] Source # many :: LogicT f a -> LogicT f [a] Source #
Applicative (LogicT f) Source # |
Instance details Defined in Control.Monad.Logic Methods pure :: a -> LogicT f a Source # (<*>) :: LogicT f (a -> b) -> LogicT f a -> LogicT f b Source # liftA2 :: (a -> b -> c) -> LogicT f a -> LogicT f b -> LogicT f c Source # (*>) :: LogicT f a -> LogicT f b -> LogicT f b Source # (<*) :: LogicT f a -> LogicT f b -> LogicT f a Source #
Functor (LogicT f) Source # |
Instance details Defined in Control.Monad.Logic Methods fmap :: (a -> b) -> LogicT f a -> LogicT f b Source # (<$) :: a -> LogicT f b -> LogicT f a Source #
Monad (LogicT m) Source # |
Instance details Defined in Control.Monad.Logic Methods (>>=) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b Source # (>>) :: LogicT m a -> LogicT m b -> LogicT m b Source # return :: a -> LogicT m a Source #
MonadPlus (LogicT m) Source # |
Instance details Defined in Control.Monad.Logic Methods mzero :: LogicT m a Source # mplus :: LogicT m a -> LogicT m a -> LogicT m a Source #
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 Source # mappend :: LogicT m a -> LogicT m a -> LogicT m a Source # mconcat :: [LogicT m a] -> LogicT m a Source #
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 Source # sconcat :: NonEmpty (LogicT m a) -> LogicT m a Source # stimes :: Integral b => b -> LogicT m a -> LogicT m a Source #

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