A backtracking, logic programming monad.
This package offers one implementation of MonadLogic: LogicT. Other notable implementations:
https://hackage.haskell.org/package/list-t/docs/ListT.html#t:ListT
https://hackage.haskell.org/package/logict-sequence/docs/Control-Monad-Logic-Sequence.html#t:SeqT
https://hackage.haskell.org/package/logict-state/docs/Control-Monad-LogicState.html#t:LogicStateT
https://hackage.haskell.org/package/streamt/docs/Control-Monad-Stream.html#t:StreamT
Methods
msplit :: m a -> m (Maybe (a, m a))Attempts to split the computation, giving access to the first result. Satisfies the following laws:
msplit empty == pure Nothing msplit (pure a <|> m) == pure (Just (a, m))interleave :: m a -> m a -> m aFair disjunction. It is possible for a logical computation to have an infinite number of potential results, for instance:
odds = pure 1 <|> fmap (+ 2) oddsSuch computations can cause problems in some circumstances. Consider:
two = do x <- odds <|> pure 2 if even x then pure x else emptyExample1 expression observe two...never completes...
Such a computation may never consider pure
2, and therefore even observetwowill never return any results. By contrast, using interleave in place of <|> ensures fair consideration of both branches of a disjunction.fairTwo = do x <- odds `interleave` pure 2 if even x then pure x else emptyExample1 expression observe fairTwo2
Note that even with interleave this computation will never terminate after returning 2: only the first value can be safely observed, after which each odd value becomes empty (equivalent to Prolog's fail) which does not stop the evaluation but indicates there is no value to return yet.
Unlike <|>, interleave is not associative:
Example5 expressions let x = [1,2,3]; y = [4,5,6]; z = [7,8,9] :: [Int]x `interleave` y[1,4,2,5,3,6](x `interleave` y) `interleave` z[1,7,4,8,2,9,5,3,6]y `interleave` z[4,7,5,8,6,9]x `interleave` (y `interleave` z)[1,4,2,7,3,5,8,6,9]
(>>-) :: m a -> (a -> m b) -> m binfixl 1Fair conjunction. Similarly to the previous function, consider the distributivity law, naturally expected from MonadPlus:
(a <|> b) >>= k = (a >>= k) <|> (b >>= k)If
a>>=kcan backtrack arbitrarily many times,b>>=kmay never be considered. In logic statements, "backtracking" is the process of discarding the current possible solution value and returning to a previous decision point where a new value can be obtained and tried. For example:Example1 expression do { x <- pure 0 <|> pure 1 <|> pure 2; if even x then pure x else empty } :: [Int][0,2]
Here, the
xvalue can be produced three times, where <|> represents the decision points of that production. The subsequentifstatement specifies empty (fail) ifxis odd, causing it to be discarded and a return to an <|> decision point to get the nextx.The statement "
a>>=kcan backtrack arbitrarily many times" means that the computation is resulting in empty and thatahas an infinite number of <|> applications to return to. This is called a conjunctive computation because the logic foraandkmust both succeed (i.e. pure a value instead of empty).Similar to the way interleave allows both branches of a disjunctive computation, the >>- operator takes care to consider both branches of a conjunctive computation.
Consider the operation:
odds = pure 1 <|> fmap (2 +) odds oddsPlus n = odds >>= \a -> pure (a + n) g = do x <- (pure 0 <|> pure 1) >>= oddsPlus if even x then pure x else emptyExample1 expression observeMany 3 g...never completes...
This will never produce any value because all values produced by the
doprogram come from the pure1driven operation (adding one to the sequence of odd values, resulting in the even values that are allowed by the test in the second line), but the pure0input tooddsPlusgenerates an infinite number of empty failures so the even values generated by the pure1alternative are never seen. Using interleave here instead of <|> does not help due to the aforementioned distributivity law.Also note that the
donotation desugars to >>= bind operations, so the following would also fail:do a <- pure 0 <|> pure 1 x <- oddsPlus a if even x then pure x else emptyThe solution is to use the >>- in place of the normal monadic bind operation >>= when fairness between alternative productions is needed in a conjunction of statements (rules):
h = do x <- (pure 0 <|> pure 1) >>- oddsPlus if even x then pure x else emptyExample1 expression observeMany 3 h[2,4,6]
However, a bit of care is needed when using >>- because, unlike >>=, it is not associative. For example:
Example7 expressions let m = [2,7] :: [Int]let k x = [x, x + 1]let h x = [x, x * 2]m >>= (\x -> k x >>= h)[2,4,3,6,7,14,8,16](m >>= k) >>= h -- same as above[2,4,3,6,7,14,8,16]m >>- (\x -> k x >>- h)[2,7,3,8,4,14,6,16](m >>- k) >>- h -- central elements are different[2,7,4,3,14,8,6,16]
This means that the following will be productive:
(pure 0 <|> pure 1) >>- oddsPlus >>- \x -> if even x then pure x else emptyWhich is equivalent to
((pure 0 <|> pure 1) >>- oddsPlus) >>- (\x -> if even x then pure x else empty)But the following will not be productive:
(pure 0 <|> pure 1) >>- (\a -> (oddsPlus a >>- \x -> if even x then pure x else empty))Since do notation desugaring results in the latter, the
RebindableSyntaxorQualifiedDolanguage pragmas cannot easily be used either. Instead, it is recommended to carefully use explicit >>- only when needed.Here is an action of
(>>-)on lists:Example1 expression take 20 $ [100,200..500] >>- (\x -> map (x +) [1..])[101,201,102,301,103,202,104,401,105,203,106,302,107,204,108,501,109,205,110,303]
The result is
map (100 +) [1..]interleaved with[200,300..500] >>- (x -> map (x +) [1..]). You can see that a half of the numbers starts from 1, a quarter starts from 2, and so on exponentially. One could argue that(>>-)is a very unfair conjunction!once :: m a -> m aPruning. Selects one result out of many. Useful for when multiple results of a computation will be equivalent, or should be treated as such.
As an example, here's a way to determine if a number is composite (has non-trivial integer divisors, i.e. not a prime number):
choose = foldr ((<|>) . pure) empty divisors n = do a <- choose [2..n-1] b <- choose [2..n-1] guard (a * b == n) pure (a, b) composite_ v = do _ <- divisors v pure "Composite"While this works as intended, it actually does too much work:
Example1 expression observeAll (composite_ 20)["Composite", "Composite", "Composite", "Composite"]
Because there are multiple divisors of 20, and they can also occur in either order:
Example1 expression observeAll (divisors 20)[(2,10), (4,5), (5,4), (10,2)]
Clearly one could just use observe here to get the first non-prime result, but if the call to
compositeis in the middle of other logic code then use once instead.composite v = do _ <- once (divisors v) pure "Composite"Example1 expression observeAll (composite 20)["Composite"]
lnot :: m a -> m ()Inverts a logic computation. If
msucceeds with at least one value, lnotmfails. Ifmfails, then lnotmsucceeds with the value().For example, evaluating if a number is prime can be based on the failure to find divisors of a number:
choose = foldr ((<|>) . pure) empty divisors n = do d <- choose [2..n-1] guard (n `rem` d == 0) pure d prime v = do _ <- lnot (divisors v) pure TrueExample2 expressions observeAll (prime 20)[]observeAll (prime 19)[True]
Here if
divisorsnever succeeds, then the lnot will succeed and the number will be declared as prime.ifte :: m a -> (a -> m b) -> m b -> m bLogical 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. The failure branch is never considered if the first argument has any successes. The ifte function satisfies the following laws:
ifte (pure a) th el == th a ifte empty th el == el ifte (pure a <|> m) th el == th a <|> (m >>= th)For example, the previous
primefunction returned nothing if the number was not prime, but if it should return False instead, the following can be used:choose = foldr ((<|>) . pure) empty divisors n = do d <- choose [2..n-1] guard (n `rem` d == 0) pure d prime v = once (ifte (divisors v) (const (pure False)) (pure True))Example2 expressions observeAll (prime 20)[False]observeAll (prime 19)[True]
Notice that this cannot be done with a simple
if-then-elsebecausedivisorseither generates values or it does not, so there's no "false" condition to check with a simpleifstatement.
Instances7MonadLogic, …
MonadLogic LogicDefined in logict-0.8.2.0 · Control.Monad.LogicMonadLogic []Defined in logict-0.8.2.0 · Control.Monad.Logic.ClassMonad m => MonadLogic (LogicT m)Defined in logict-0.8.2.0 · Control.Monad.LogicMonadLogic m => MonadLogic (ReaderT e m)Defined in logict-0.8.2.0 · Control.Monad.Logic.ClassNote that splitting a transformer does not allow you to provide different input to the monadic object returned. For instance, in:
let Just (_, rm') = runReaderT (msplit rm) r in runReaderT rm' r'r'will be ignored, becauserwas already threaded through the computation.(Monoid w, MonadLogic m, MonadPlus m) => MonadLogic (WriterT w m)Defined in logict-0.8.2.0 · Control.Monad.Logic.Class(MonadLogic m, MonadPlus m) => MonadLogic (StateT s m)Defined in logict-0.8.2.0 · Control.Monad.Logic.ClassSee note on splitting above.
(MonadLogic m, MonadPlus m) => MonadLogic (StateT s m)Defined in logict-0.8.2.0 · Control.Monad.Logic.ClassSee note on splitting above.