logict 0.7.0.3 → 0.7.1.0
raw patch · 8 files changed
+1095/−126 lines, 8 filesdep +asyncdep +transformersdep ~basedep ~mtlnew-component:exe:grandparents
Dependencies added: async, transformers
Dependency ranges changed: base, mtl
Files
- Control/Monad/Logic.hs +117/−42
- Control/Monad/Logic/Class.hs +287/−62
- LICENSE +6/−1
- README.md +125/−0
- changelog.md +5/−0
- example/grandparents.hs +29/−0
- logict.cabal +28/−16
- test/Test.hs +498/−5
Control/Monad/Logic.hs view
@@ -1,16 +1,21 @@ ------------------------------------------------------------------------- -- | -- Module : Control.Monad.Logic--- Copyright : (c) Dan Doel+-- 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> ----- A backtracking, logic programming monad.------ Adapted from the paper--- /Backtracking, Interleaving, and Terminating Monad Transformers/,--- by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry--- (<http://okmij.org/ftp/papers/LogicT.pdf>).+-- Adapted from the paper+-- <http://okmij.org/ftp/papers/LogicT.pdf 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'. ------------------------------------------------------------------------- {-# LANGUAGE CPP #-}@@ -19,7 +24,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE UndecidableInstances #-} -#if __GLASGOW_HASKELL__ >= 702+#if __GLASGOW_HASKELL__ >= 704 {-# LANGUAGE Safe #-} #endif @@ -39,19 +44,21 @@ observeManyT, observeAllT, module Control.Monad,- module Control.Monad.Trans+ module Trans ) where import Control.Applicative import Control.Monad import qualified Control.Monad.Fail as Fail-import Control.Monad.Identity-import Control.Monad.Trans+import Control.Monad.Identity (Identity(..))+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Trans (MonadTrans(..))+import qualified Control.Monad.Trans as Trans -import Control.Monad.Reader.Class-import Control.Monad.State.Class-import Control.Monad.Error.Class+import Control.Monad.Reader.Class (MonadReader(..))+import Control.Monad.State.Class (MonadState(..))+import Control.Monad.Error.Class (MonadError(..)) #if !MIN_VERSION_base(4,8,0) import Data.Monoid (Monoid (..))@@ -73,8 +80,8 @@ LogicT { unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r } ---------------------------------------------------------------------------- | Extracts the first result from a LogicT computation,--- failing otherwise.+-- | Extracts the first result from a 'LogicT' computation,+-- failing if there are no results at all. #if !MIN_VERSION_base(4,13,0) observeT :: Monad m => LogicT m a -> m a #else@@ -83,12 +90,33 @@ observeT lt = unLogicT lt (const . return) (fail "No answer.") ---------------------------------------------------------------------------- | Extracts all results from a LogicT computation.-observeAllT :: Monad m => LogicT m a -> m [a]-observeAllT m = unLogicT m (liftM . (:)) (return [])+-- | 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', 'Control.Monad.Reader.Reader',+-- 'Control.Monad.Writer.Writer', and 'Control.Monad.State.State')+-- will be productive:+--+-- >>> take 5 $ runIdentity (observeAllT nats)+-- [0,1,2,3,4]+--+-- but others (like 'Control.Monad.Except.ExceptT',+-- and 'Control.Monad.Cont.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.+observeAllT :: Applicative m => LogicT m a -> m [a]+observeAllT m = unLogicT m (fmap . (:)) (pure []) ---------------------------------------------------------------------------- | Extracts up to a given number of results from a LogicT computation.+-- | Extracts up to a given number of results from a 'LogicT' computation. observeManyT :: Monad m => Int -> LogicT m a -> m [a] observeManyT n m | n <= 0 = return []@@ -99,43 +127,89 @@ sk (Just (a, m')) _ = (a:) `liftM` observeManyT (n-1) m' ---------------------------------------------------------------------------- | Runs a LogicT computation with the specified initial success and+-- | 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+-- runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r runLogicT (LogicT r) = r ---------------------------------------------------------------------------- | The basic Logic monad, for performing backtracking computations--- returning values of type @a@.+-- | The basic 'Logic' monad, for performing backtracking computations+-- returning values (e.g. 'Logic' @a@ will return values of type @a@). type Logic = LogicT Identity ---------------------------------------------------------------------------- | A smart constructor for Logic computations.+-- | A smart constructor for 'Logic' computations. logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a logic f = LogicT $ \k -> Identity . f (\a -> runIdentity . k a . Identity) . runIdentity ---------------------------------------------------------------------------- | Extracts the first result from a Logic computation.+-- | 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.+-- observe :: Logic a -> a-observe lt = runIdentity $ unLogicT lt (const . return) (error "No answer.")+observe lt = runIdentity $ unLogicT lt (const . pure) (error "No answer.") ---------------------------------------------------------------------------- | Extracts all results from a Logic computation.+-- | Extracts all results from a 'Logic' computation.+--+-- >>> observe (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)+-- [5,3]+-- observeAll :: Logic a -> [a] observeAll = runIdentity . observeAllT ---------------------------------------------------------------------------- | Extracts up to a given number of results from a Logic computation.+-- | 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]+-- observeMany :: Int -> Logic a -> [a] observeMany i = take i . observeAll -- Implementing 'observeMany' using 'observeManyT' is quite costly, -- because it calls 'msplit' multiple times. ---------------------------------------------------------------------------- | Runs a Logic computation with the specified initial success and+-- | Runs a 'Logic' computation with the specified initial success and -- failure continuations.+--+-- >>> runLogic empty (+) 0+-- 0+--+-- >>> runLogic (pure 5 <|> pure 3 <|> empty) (+) 0+-- 8+-- runLogic :: Logic a -> (a -> r -> r) -> r -> r runLogic l s f = runIdentity $ unLogicT l si fi where@@ -154,7 +228,7 @@ f1 <|> f2 = LogicT $ \sk fk -> unLogicT f1 sk (unLogicT f2 sk fk) instance Monad (LogicT m) where- return a = LogicT $ \sk fk -> sk a fk+ return = pure m >>= f = LogicT $ \sk fk -> unLogicT m (\a fk' -> unLogicT (f a) sk fk') fk #if !MIN_VERSION_base(4,13,0) fail = Fail.fail@@ -164,8 +238,8 @@ fail _ = LogicT $ \_ fk -> fk instance MonadPlus (LogicT m) where- mzero = LogicT $ \_ fk -> fk- m1 `mplus` m2 = LogicT $ \sk fk -> unLogicT m1 sk (unLogicT m2 sk fk)+ mzero = empty+ mplus = (<|>) #if MIN_VERSION_base(4,9,0) instance Semigroup (LogicT m a) where@@ -174,9 +248,9 @@ #endif instance Monoid (LogicT m a) where- mempty = mzero- mappend = mplus- mconcat = foldr mplus mzero+ mempty = empty+ mappend = (<|>)+ mconcat = F.asum instance MonadTrans LogicT where lift m = LogicT $ \sk fk -> m >>= \a -> sk a fk@@ -189,28 +263,29 @@ -- Try to avoid it. msplit m = lift $ unLogicT m ssk (return Nothing) where- ssk a fk = return $ Just (a, (lift fk >>= reflect))+ ssk a fk = return $ Just (a, lift fk >>= reflect) once m = LogicT $ \sk fk -> unLogicT m (\a _ -> sk a fk) fk lnot m = LogicT $ \sk fk -> unLogicT m (\_ _ -> fk) (sk () fk) #if MIN_VERSION_base(4,8,0) -instance {-# OVERLAPPABLE #-} (Monad m, F.Foldable m) => F.Foldable (LogicT m) where- foldMap f m = F.fold $ unLogicT m (liftM . mappend . f) (return mempty)+instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where+ foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty) instance {-# OVERLAPPING #-} F.Foldable (LogicT Identity) where foldr f z m = runLogic m f z #else -instance (Monad m, F.Foldable m) => F.Foldable (LogicT m) where- foldMap f m = F.fold $ unLogicT m (liftM . mappend . f) (return mempty)+instance (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where+ foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty) #endif instance T.Traversable (LogicT Identity) where- traverse g l = runLogic l (\a ft -> cons <$> g a <*> ft) (pure mzero)- where cons a l' = return a `mplus` l'+ traverse g l = runLogic l (\a ft -> cons <$> g a <*> ft) (pure empty)+ where+ cons a l' = pure a <|> l' -- Needs undecidable instances instance MonadReader r m => MonadReader r (LogicT m) where
Control/Monad/Logic/Class.hs view
@@ -1,113 +1,338 @@ ------------------------------------------------------------------------- -- | -- Module : Control.Monad.Logic.Class--- Copyright : (c) Dan Doel+-- 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> ----- A backtracking, logic programming monad.------ Adapted from the paper--- /Backtracking, Interleaving, and Terminating Monad Transformers/,--- by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry--- (<http://okmij.org/ftp/papers/LogicT.pdf>).+-- Adapted from the paper+-- <http://okmij.org/ftp/papers/LogicT.pdf 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'. ------------------------------------------------------------------------- -{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP #-} -#if __GLASGOW_HASKELL__ >= 702+#if __GLASGOW_HASKELL__ >= 704 {-# LANGUAGE Safe #-} #endif module Control.Monad.Logic.Class (MonadLogic(..), reflect) where -import Control.Monad.Reader+import Control.Applicative+import Control.Monad+import Control.Monad.Reader (ReaderT(..))+import Control.Monad.Trans (MonadTrans(..)) import qualified Control.Monad.State.Lazy as LazyST import qualified Control.Monad.State.Strict as StrictST ----------------------------------------------------------------------------------- | Minimal implementation: msplit-class (MonadPlus m) => MonadLogic m where- -- | Attempts to split the computation, giving access to the first+-- | A backtracking, logic programming monad.+class (Monad m, Alternative m) => MonadLogic m where+ -- | 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))+ -- > msplit empty == pure Nothing+ -- > msplit (pure a <|> m) == pure (Just (a, m)) msplit :: m a -> m (Maybe (a, m a)) - -- | Fair disjunction. It is possible for a logical computation+ -- | __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+ -- > odds = pure 1 <|> fmap (+ 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+ -- > two = do x <- odds <|> pure 2+ -- > if even x then pure x else empty --- -- 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+ -- >>> observe two+ -- ...never completes...+ --+ -- Such a computation may never consider 'pure' @2@, and+ -- therefore even 'Control.Monad.Logic.observe' @two@ will+ -- never return any results. By+ -- contrast, using 'interleave' in place of+ -- 'Control.Applicative.<|>' ensures fair consideration of both+ -- branches of a disjunction.+ --+ -- > fairTwo = do x <- odds `interleave` pure 2+ -- > if even x then pure x else empty+ --+ -- >>> observe fairTwo+ -- 2+ --+ -- 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 'Control.Applicative.empty'+ -- (equivalent to+ -- <http://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse45 Prolog's fail>)+ -- which does not stop the evaluation but indicates there is no+ -- value to return yet.+ --+ -- Unlike '<|>', 'interleave' is not associative:+ --+ -- >>> 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]+ -- interleave :: m a -> m a -> m a - -- | Fair conjunction. Similarly to the previous function, consider- -- the distributivity law for MonadPlus:+ -- | __Fair conjunction.__ Similarly to the previous function, consider+ -- the distributivity law, naturally expected from 'MonadPlus': --- -- > (mplus a b) >>= k = (a >>= k) `mplus` (b >>= k)+ -- > (a <|> b) >>= k = (a >>= k) <|> (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.+ -- If @a@ '>>=' @k@ can backtrack arbitrarily many times, @b@ '>>=' @k@+ -- may 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:+ --+ -- >>> do { x <- pure 0 <|> pure 1 <|> pure 2; if even x then pure x else empty } :: [Int]+ -- [0,2]+ --+ -- Here, the @x@ value can be produced three times, where+ -- 'Control.Applicative.<|>' represents the decision points of that+ -- production. The subsequent @if@ statement specifies+ -- 'Control.Applicative.empty' (fail)+ -- if @x@ is odd, causing it to be discarded and a return+ -- to an 'Control.Applicative.<|>' decision point to get the next @x@.+ --+ -- The statement "@a@ '>>=' @k@ can backtrack arbitrarily many+ -- times" means that the computation is resulting in 'Control.Applicative.empty' and+ -- that @a@ has an infinite number of 'Control.Applicative.<|>' applications to+ -- return to. This is called a conjunctive computation because+ -- the logic for @a@ /and/ @k@ must both succeed (i.e. 'pure'+ -- a value instead of 'Control.Applicative.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 empty+ --+ -- >>> observeMany 3 g+ -- ...never completes...+ --+ -- This will never produce any value because all values produced+ -- by the @do@ program come from the 'pure' @1@ driven 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 'pure' @0@ input to @oddsPlus@ generates an infinite+ -- number of 'Control.Applicative.empty' failures so the even values generated by+ -- the 'pure' @1@ alternative are never seen. Using+ -- 'interleave' here instead of 'Control.Applicative.<|>' does not help due+ -- to the aforementioned distributivity law.+ --+ -- Also note that the @do@ notation 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 empty+ --+ -- The 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 empty+ --+ -- >>> observeMany 3 h+ -- [2,4,6]+ --+ -- However, a bit of care is needed when using '>>-' because,+ -- unlike '>>=', it is not associative. For example:+ --+ -- >>> 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 empty+ --+ -- Which 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+ -- @RebindableSyntax@ language pragma cannot easily be used+ -- either. Instead, it is recommended to carefully use explicit+ -- '>>-' only when needed.+ -- (>>-) :: m a -> (a -> m b) -> m b infixl 1 >>- - -- | 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)- ifte :: m a -> (a -> m b) -> m b -> m b-- -- | Pruning. Selects one result out of many. Useful for when multiple+ -- | __Pruning.__ 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+ -- <https://wikipedia.org/wiki/Composite_number 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:+ --+ -- >>> observeAll (composite_ 20)+ -- ["Composite", "Composite", "Composite", "Composite"]+ --+ -- Because there are multiple divisors of 20, and they can also+ -- occur in either order:+ --+ -- >>> observeAll (divisors 20)+ -- [(2,10), (4,5), (5,4), (10,2)]+ --+ -- Clearly one could just use 'Control.Monad.Logic.observe' here to get the first+ -- non-prime result, but if the call to @composite@ is in the+ -- middle of other logic code then use 'once' instead.+ --+ -- > composite v = do _ <- once (divisors v)+ -- > pure "Composite"+ --+ -- >>> observeAll (composite 20)+ -- ["Composite"]+ -- once :: m a -> m a - -- | Inverts a logic computation. If @m@ succeeds with at least one value,- -- @lnot m@ fails. If @m@ fails, then @lnot m@ succeeds the value @()@.+ -- | __Inverts__ a logic computation. If @m@ succeeds with at least one value,+ -- 'lnot' @m@ fails. If @m@ fails, then 'lnot' @m@ succeeds 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 True+ --+ -- >>> observeAll (prime 20)+ -- []+ -- >>> observeAll (prime 19)+ -- [True]+ --+ -- Here if @divisors@ never succeeds, then the 'lnot' will+ -- succeed and the number will be declared as prime. lnot :: m a -> m () + -- | Logical __conditional.__ The equivalent of+ -- <http://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse44 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 @prime@ function 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 True))+ -- > (pure False))+ --+ -- >>> observeAll (prime 20)+ -- [False]+ -- >>> observeAll (prime 19)+ -- [True]+ --+ -- Notice that this cannot be done with a simple @if-then-else@+ -- because @divisors@ either generates values or it does not, so+ -- there's no "false" condition to check with a simple @if@+ -- statement.+ ifte :: m a -> (a -> m b) -> m b -> m b+ -- All the class functions besides msplit can be derived from msplit, if -- desired interleave m1 m2 = msplit m1 >>=- maybe m2 (\(a, m1') -> return a `mplus` interleave m2 m1')+ maybe m2 (\(a, m1') -> pure a <|> interleave m2 m1') - m >>- f = do (a, m') <- maybe mzero return =<< msplit m+ m >>- f = do (a, m') <- maybe empty pure =<< msplit m interleave (f a) (m' >>- f) - ifte t th el = msplit t >>= maybe el (\(a,m) -> th a `mplus` (m >>= th))+ ifte t th el = msplit t >>= maybe el (\(a,m) -> th a <|> (m >>= th)) - once m = do (a, _) <- maybe mzero return =<< msplit m- return a+ once m = do (a, _) <- maybe empty pure =<< msplit m+ pure a - lnot m = ifte (once m) (const mzero) (return ())+ lnot m = ifte (once m) (const empty) (pure ()) ---------------------------------------------------------------------------------- | The inverse of msplit. Satisfies the following law:+-- | The inverse of 'msplit'. Satisfies the following law: -- -- > msplit m >>= reflect == m-reflect :: MonadLogic m => Maybe (a, m a) -> m a-reflect Nothing = mzero-reflect (Just (a, m)) = return a `mplus` m+reflect :: Alternative m => Maybe (a, m a) -> m a+reflect Nothing = empty+reflect (Just (a, m)) = pure a <|> m -- An instance of MonadLogic for lists instance MonadLogic [] where- msplit [] = return Nothing- msplit (x:xs) = return $ Just (x, xs)+ msplit [] = pure Nothing+ msplit (x:xs) = pure $ Just (x, xs) -- | Note that splitting a transformer does -- not allow you to provide different input@@ -121,17 +346,17 @@ instance MonadLogic m => MonadLogic (ReaderT e m) where msplit rm = ReaderT $ \e -> do r <- msplit $ runReaderT rm e case r of- Nothing -> return Nothing- Just (a, m) -> return (Just (a, lift m))+ Nothing -> pure Nothing+ Just (a, m) -> pure (Just (a, lift m)) -- | See note on splitting above.-instance MonadLogic m => MonadLogic (StrictST.StateT s m) where+instance (MonadLogic m, MonadPlus m) => MonadLogic (StrictST.StateT s m) where msplit sm = StrictST.StateT $ \s -> do r <- msplit (StrictST.runStateT sm s) case r of- Nothing -> return (Nothing, s)+ Nothing -> pure (Nothing, s) Just ((a,s'), m) ->- return (Just (a, StrictST.StateT (\_ -> m)), s')+ pure (Just (a, StrictST.StateT (const m)), s') interleave ma mb = StrictST.StateT $ \s -> StrictST.runStateT ma s `interleave` StrictST.runStateT mb s@@ -146,13 +371,13 @@ once ma = StrictST.StateT $ \s -> once (StrictST.runStateT ma s) -- | See note on splitting above.-instance MonadLogic m => MonadLogic (LazyST.StateT s m) where+instance (MonadLogic m, MonadPlus m) => MonadLogic (LazyST.StateT s m) where msplit sm = LazyST.StateT $ \s -> do r <- msplit (LazyST.runStateT sm s) case r of- Nothing -> return (Nothing, s)+ Nothing -> pure (Nothing, s) Just ((a,s'), m) ->- return (Just (a, LazyST.StateT (\_ -> m)), s')+ pure (Just (a, LazyST.StateT (const m)), s') interleave ma mb = LazyST.StateT $ \s -> LazyST.runStateT ma s `interleave` LazyST.runStateT mb s
LICENSE view
@@ -1,6 +1,11 @@ This module is under this "3 clause" BSD license: -Copyright (c) 2007-2010, Dan Doel+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 All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+ README.md view
@@ -0,0 +1,125 @@+# logict [](https://github.com/Bodigrim/logict/actions?query=workflow%3AHaskell-CI) [](https://hackage.haskell.org/package/logict) [](http://stackage.org/lts/package/logict) [](http://stackage.org/nightly/package/logict)++Provides support for logic-based evaluation. Logic-based programming+uses a technique known as backtracking to consider alternative values+as solutions to logic statements, and is exemplified by languages+such as [Prolog](https://wikipedia.org/wiki/Prolog) and+[Datalog](https://wikipedia.org/wiki/Datalog).++Logic-based programming replaces explicit iteration and sequencing+code with implicit functionality that internally "iterates" (via+backtracking) over a set of possible values that satisfy explicitly+provided conditions.++This package adds support for logic-based programming in Haskell using+the continuation-based techniques adapted from the paper+[Backtracking, Interleaving, and Terminating Monad Transformers](http://okmij.org/ftp/papers/LogicT.pdf)+by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry.+This paper extends previous research into using `MonadPlus`+functionality—where `mplus` is used to specify value alternatives+for consideration and `mzero` use used to specify the lack of any+acceptable values—to add support for fairness and pruning using a+set of operations defined by a new `MonadLogic` class.++# Background++In a typical example for Prolog logic programming, there are a set of+facts (expressed as unconditional statements):++```prolog+parent(sarah, john).+parent(arnold, john).+parent(john, anne).+```++and a set of rules that apply if their conditions (body clause) are satisfied:++```prolog+grandparent(Person, Grandchild) :- parent(Person, X), parent(X, Grandchild).+```++Execution of a query for this rule `grandparent(G, anne)` would result in the following "values":++```prolog+grandparent(sarah, anne).+grandparent(arnold, anne).+```++For this query execution, `Person` and `X` are "free" variables where+`Grandchild` has been fixed to `anne`. The Prolog engine internally+"backtracks" to the `parent(Person, X)` statement to try different+known values for each variable, executing forward to see if the values+satisfy all the results and produce a resulting value.++# Haskell logict Package++The Haskell equivalent for the example above, using the `logict` package+might look something like the following:++```haskell+import Control.Applicative+import Control.Monad.Logic++parents :: [ (String, String) ]+parents = [ ("Sarah", "John")+ , ("Arnold", "John")+ , ("John", "Anne")+ ]++grandparent :: String -> Logic String+grandparent grandchild = do (p, c) <- choose parents+ (c', g) <- choose parents+ guard (c == c')+ guard (g == grandchild)+ pure p++choose = foldr ((<|>) . pure) empty++main = do let grandparents = observeAll (grandparent "Anne")+ putStrLn $ "Anne's grandparents are: " <> show grandparents+```++In this simple example, each of the `choose` calls acts as a+backtracking choice point where different entries of the `parents`+array will be generated. This backtracking is handled automatically+by the `MonadLogic` instance for `Logic` and does not need to be+explicitly written into the code. The `observeAll` function collects+all the values "produced" by `Logic`, allowing this program to+display:++```+Anne's grandparents are: ["Sarah","Arnold"]+```++This example is provided as the `grandparents` executable built by the+`logict` package so you can run it yourself and try various+experimental modifications.++The example above is very simplistic and is just a brief introduction+into the capabilities of logic programming and the `logict` package.+The `logict` package provides additional functionality such as:++ * Fair conjunction and disjunction, which can help with potentially+ infinite sets of inputs.++ * A `LogicT` monad stack that lets logic operations be performed+ along with other monadic actions (e.g. if the parents sample was+ streamed from an input file using the `IO` monad).++ * A `MonadLogic` class which allows other monads to be defined which+ provide logic programming capabilities.++## Additional Notes++The implementation in this `logict` package provides the backtracking+functionality at a lower level than that defined in the associated+paper. The backtracking is defined within the `Alternative` class as+`<|>` and `empty`, whereas the paper uses the `MonadPlus` class and+the `mplus` and `mzero` functions; since `Alternative` is a+requirement (constraint) for `MonadPlus`, this allows both+nomenclatures to be supported and used as appropriate to the client+code.++More details on using this package as well as other functions+(including fair conjunction and disjunction) are provided in the+[Haddock documentation](https://hackage.haskell.org/package/logict).
changelog.md view
@@ -1,3 +1,8 @@+# 0.7.1.0++* Improve documentation.+* Relax superclasses of `MonadLogic` to `Monad` and `Alternative` instead of `MonadPlus`.+ # 0.7.0.3 * Support GHC 9.0.
+ example/grandparents.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE CPP #-}++import Control.Applicative+import Control.Monad.Logic+#if !MIN_VERSION_base(4,8,0)+import Data.Monoid (Monoid (..))+#endif+#if MIN_VERSION_base(4,9,0)+import Data.Semigroup (Semigroup (..))+#endif+++parents :: [ (String, String) ]+parents = [ ("Sarah", "John")+ , ("Arnold", "John")+ , ("John", "Anne")+ ]++grandparent :: String -> Logic String+grandparent grandchild = do (p, c) <- choose parents+ (c', g) <- choose parents+ guard (c == c')+ guard (g == grandchild)+ pure p++choose = foldr ((<|>) . pure) empty++main = do let grandparents = observeAll (grandparent "Anne")+ putStrLn $ "Anne's grandparents are: " ++ show grandparents
logict.cabal view
@@ -1,27 +1,28 @@ name: logict-version: 0.7.0.3+version: 0.7.1.0 license: BSD3 license-file: LICENSE copyright:- Copyright (c) 2007-2014, Dan Doel,- Copyright (c) 2011-2013, Edward Kmett,- Copyright (c) 2014, Roman Cheplyaka+ (c) 2007-2014 Dan Doel,+ (c) 2011-2013 Edward Kmett,+ (c) 2014 Roman Cheplyaka,+ (c) 2020-2021 Andrew Lelechenko,+ (c) 2020-2021 Kevin Quick maintainer: Andrew Lelechenko <andrew.lelechenko@gmail.com> author: Dan Doel homepage: https://github.com/Bodigrim/logict#readme synopsis: A backtracking logic-programming monad. description:- A continuation-based, backtracking, logic programming monad.- An adaptation of the two-continuation implementation found- in the paper "Backtracking, Interleaving, and Terminating- Monad Transformers" available here:- <http://okmij.org/ftp/papers/LogicT.pdf>+ Adapted from the paper+ <http://okmij.org/ftp/papers/LogicT.pdf Backtracking, Interleaving, and Terminating Monad Transformers>+ by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry. category: Control build-type: Simple extra-source-files: changelog.md+ README.md cabal-version: >=1.10-tested-with: GHC ==7.4.2 GHC ==7.6.3 GHC ==7.8.4 GHC ==7.10.3 GHC ==8.0.2 GHC ==8.2.2 GHC ==8.4.4 GHC ==8.6.5 GHC ==8.8.3 GHC ==8.10.1+tested-with: GHC ==7.0.4 GHC ==7.2.2 GHC ==7.4.2 GHC ==7.6.3 GHC ==7.8.4 GHC ==7.10.3 GHC ==8.0.2 GHC ==8.2.2 GHC ==8.4.4 GHC ==8.6.5 GHC ==8.8.4 GHC ==8.10.3 source-repository head type: git@@ -34,22 +35,33 @@ default-language: Haskell2010 ghc-options: -O2 -Wall build-depends:- base >=2 && <5,- mtl >=2 && <2.3+ base >=4.3 && <5,+ mtl >=2.0 && <2.3 if impl(ghc <8.0) build-depends:- fail -any+ fail, transformers +executable grandparents+ buildable: False+ main-is: grandparents.hs+ hs-source-dirs: example+ default-language: Haskell2010+ build-depends:+ base,+ logict+ test-suite logict-tests type: exitcode-stdio-1.0 main-is: Test.hs default-language: Haskell2010 ghc-options: -Wall build-depends:- base >=2 && <5,- logict -any,- mtl >=2 && <2.3,+ base,+ async >=2.0,+ logict,+ mtl, tasty, tasty-hunit+ hs-source-dirs: test
test/Test.hs view
@@ -1,13 +1,32 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} module Main where -import Test.Tasty-import Test.Tasty.HUnit+import Test.Tasty+import Test.Tasty.HUnit -import Control.Monad.Logic-import Control.Monad.Reader+import Control.Arrow ( left )+import Control.Concurrent ( threadDelay )+import Control.Concurrent.Async ( race )+import Control.Exception+import Control.Monad.Identity+import Control.Monad.Logic+import Control.Monad.Reader+import qualified Control.Monad.State.Lazy as SL+import qualified Control.Monad.State.Strict as SS+import Data.Maybe +#if MIN_VERSION_base(4,9,0)+#if MIN_VERSION_base(4,11,0)+#else+import Data.Semigroup (Semigroup (..))+#endif+#else+import Data.Monoid+#endif++ monadReader1 :: Assertion monadReader1 = assertEqual "should be equal" [5 :: Int] $ runReader (observeAllT (local (+ 5) ask)) 0@@ -22,8 +41,482 @@ y <- ask return (x,y) +monadReader3 :: Assertion+monadReader3 = assertEqual "should be equal" [5,3] $+ runReader (observeAllT (plus5 `mplus` mzero `mplus` plus3)) (0 :: Int)+ where+ plus5 = local (5+) ask+ plus3 = local (3+) ask++nats, odds, oddsOrTwo,+ oddsOrTwoUnfair, oddsOrTwoFair,+ odds5down :: Monad m => LogicT m Integer++#if MIN_VERSION_base(4,8,0)+nats = pure 0 `mplus` ((1 +) <$> nats)+#else+nats = return 0 `mplus` liftM (1 +) nats+#endif++odds = return 1 `mplus` liftM (2+) odds++oddsOrTwoUnfair = odds `mplus` return 2+oddsOrTwoFair = odds `interleave` return 2++oddsOrTwo = do x <- oddsOrTwoFair+ if even x then once (return x) else mzero++odds5down = return 5 `mplus` mempty `mplus` mempty `mplus` return 3 `mplus` return 1++yieldWords :: [String] -> LogicT m String+yieldWords = go+ where go [] = mzero+ go (w:ws) = return w `mplus` go ws++ main :: IO ()-main = defaultMain $ testGroup "All"+main = defaultMain $+#if __GLASGOW_HASKELL__ >= 702+ localOption (mkTimeout 3000000) $ -- 3 second deadman timeout+#endif+ testGroup "All"+ [ testGroup "Monad Reader + env" [ testCase "Monad Reader 1" monadReader1 , testCase "Monad Reader 2" monadReader2+ , testCase "Monad Reader 3" monadReader3 ]++ , testGroup "Various monads"+ [+ -- nats will generate an infinite number of results; demonstrate+ -- various ways of observing them via Logic/LogicT+ testCase "runIdentity all" $ [0..4] @=? (take 5 $ runIdentity $ observeAllT nats)+ , testCase "runIdentity many" $ [0..4] @=? (runIdentity $ observeManyT 5 nats)+ , testCase "observeAll" $ [0..4] @=? (take 5 $ observeAll nats)+ , testCase "observeMany" $ [0..4] @=? (observeMany 5 nats)++ -- Ensure LogicT can be run over other base monads other than+ -- List. Some are productive (Reader) and some are non-productive+ -- (ExceptT, ContT) in the observeAll case.++ , testCase "runReader is productive" $+ [0..4] @=? (take 5 $ runReader (observeAllT nats) "!")++ , testCase "observeManyT can be used with Either" $+ (Right [0..4] :: Either Char [Integer]) @=?+ (observeManyT 5 nats)+ ]++ --------------------------------------------------++ , testGroup "Control.Monad.Logic tests"+ [+ testCase "runLogicT multi" $ ["Hello world !"] @=?+ let conc w o = fmap ((w `mappend` " ") `mappend`) o in+ (runLogicT (yieldWords ["Hello", "world"]) conc (return "!"))++ , testCase "runLogicT none" $ ["!"] @=?+ let conc w o = fmap ((w `mappend` " ") `mappend`) o in+ (runLogicT (yieldWords []) conc (return "!"))++ , testCase "runLogicT first" $ ["Hello"] @=?+ (runLogicT (yieldWords ["Hello", "world"]) (\w -> const $ return w) (return "!"))++ , testCase "runLogic multi" $ 20 @=? runLogic odds5down (+) 11+ , testCase "runLogic none" $ 11 @=? runLogic mzero (+) (11 :: Integer)++ , testCase "observe multi" $ 5 @=? observe odds5down+ , testCase "observe none" $ (Left "No answer." @=?) =<< safely (observe mzero)++ , testCase "observeAll multi" $ [5,3,1] @=? observeAll odds5down+ , testCase "observeAll none" $ ([] :: [Integer]) @=? observeAll mzero++ , testCase "observeMany multi" $ [5,3] @=? observeMany 2 odds5down+ , testCase "observeMany none" $ ([] :: [Integer]) @=? observeMany 2 mzero+ ]++ --------------------------------------------------++ , testGroup "Control.Monad.Logic.Class tests"+ [+ testGroup "msplit laws"+ [+ testGroup "msplit mzero == return Nothing"+ [+ testCase "msplit mzero :: []" $+ msplit mzero @=? return (Nothing :: Maybe (String, [String]))++ , testCase "msplit mzero :: ReaderT" $+ let z :: ReaderT Int [] String+ z = mzero+ in assertBool "ReaderT" $ null $ catMaybes $ runReaderT (msplit z) 0++ , testCase "msplit mzero :: LogicT" $+ let z :: LogicT [] String+ z = mzero+ in assertBool "LogicT" $ null $ catMaybes $ concat $ observeAllT (msplit z)+ , testCase "msplit mzero :: strict StateT" $+ let z :: SS.StateT Int [] String+ z = mzero+ in assertBool "strict StateT" $ null $ catMaybes $ SS.evalStateT (msplit z) 0+ , testCase "msplit mzero :: lazy StateT" $+ let z :: SL.StateT Int [] String+ z = mzero+ in assertBool "lazy StateT" $ null $ catMaybes $ SL.evalStateT (msplit z) 0+ ]++ , testGroup "msplit (return a `mplus` m) == return (Just a, m)" $+ let sample = [1::Integer,2,3] in+ [+ testCase "msplit []" $ do+ let op = sample+ extract = fmap (fmap fst)+ extract (msplit op) @?= [Just 1]+ extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= [Just 2]++ , testCase "msplit ReaderT" $ do+ let op = ask+ extract = fmap fst . catMaybes . flip runReaderT sample+ extract (msplit op) @?= [sample]+ extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= []++ , testCase "msplit LogicT" $ do+ let op :: LogicT [] Integer+ op = foldr (mplus . return) mzero sample+ extract = fmap fst . catMaybes . concat . observeAllT+ extract (msplit op) @?= [1]+ extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= [2]++ , testCase "msplit strict StateT" $ do+ let op :: SS.StateT Integer [] Integer+ op = (SS.modify (+1) >> SS.get `mplus` op)+ extract = fmap fst . catMaybes . flip SS.evalStateT 0+ extract (msplit op) @?= [1]+ extract (msplit op >>= \(Just (_,nxt)) -> msplit nxt) @?= [2]++ , testCase "msplit lazy StateT" $ do+ let op :: SL.StateT Integer [] Integer+ op = (SL.modify (+1) >> SL.get `mplus` op)+ extract = fmap fst . catMaybes . flip SL.evalStateT 0+ extract (msplit op) @?= [1]+ extract (msplit op >>= \(Just (_,nxt)) -> msplit nxt) @?= [2]+ ]+ ]++ , testGroup "fair disjunction"+ [+ -- base case+ testCase "some odds" $ [1,3,5,7] @=? observeMany 4 odds++ -- without fairness, the second producer is never considered+ , testCase "unfair disjunction" $ [1,3,5,7] @=? observeMany 4 oddsOrTwoUnfair++ -- with fairness, the results are interleaved++ , testCase "fair disjunction :: LogicT" $ [1,2,3,5] @=? observeMany 4 oddsOrTwoFair++ -- without fairness nothing would be produced, but with+ -- fairness, a production is obtained++ , testCase "fair production" $ [2] @=? observeT oddsOrTwo++ -- however, asking for additional productions will not+ -- terminate (there are none, since the first clause generates+ -- an infinity of mzero "failures")++ , testCase "NONTERMINATION even when fair" $+ (Left () @=?) =<< (nonTerminating $ observeManyT 2 oddsOrTwo)++ -- Validate fair disjunction works for other+ -- Control.Monad.Logic.Class instances++ , testCase "fair disjunction :: []" $ [1,2,3,5] @=?+ (take 4 $ let oddsL = [ 1::Integer ] `mplus` [ o | o <- [3..], odd o ]+ oddsOrTwoLFair = oddsL `interleave` [2]+ in oddsOrTwoLFair)++ , testCase "fair disjunction :: ReaderT" $ [1,2,3,5] @=?+ (take 4 $ runReaderT (let oddsR = return 1 `mplus` liftM (2+) oddsR+ in oddsR `interleave` return (2 :: Integer)) "go")++ , testCase "fair disjunction :: strict StateT" $ [1,2,3,5] @=?+ (take 4 $ SS.evalStateT (let oddsS = return 1 `mplus` liftM (2+) oddsS+ in oddsS `interleave` return (2 :: Integer)) "go")++ , testCase "fair disjunction :: lazy StateT" $ [1,2,3,5] @=?+ (take 4 $ SL.evalStateT (let oddsS = return 1 `mplus` liftM (2+) oddsS+ in oddsS `interleave` return (2 :: Integer)) "go")+ ]++ , testGroup "fair conjunction" $+ [+ -- Using the fair conjunction operator (>>-) the test produces values++ testCase "fair conjunction :: LogicT" $ [2,4,6,8] @=?+ observeMany 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ do x <- (return 0 `mplus` return 1) >>- oddsPlus+ if even x then return x else mzero+ )++ -- The first >>- results in a term that produces only a stream+ -- of evens, so the >>- can produce from that stream. The+ -- operation is effectively:+ --+ -- (interleave (return 0) (return 1)) >>- oddsPlus >>- if ...+ --+ -- And so the values produced for oddsPlus to consume are+ -- alternated between 0 and 1, allowing oddsPlus to produce a+ -- value for every 1 received.++ , testCase "fair conjunction OK" $ [2,4,6,8] @=?+ observeMany 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ (return 0 `mplus` return 1) >>-+ oddsPlus >>-+ (\x -> if even x then return x else mzero)+ )++ -- This demonstrates that there is no choice to be made for+ -- oddsPlus productions in the above and >>- is effectively >>=.++ , testCase "fair conjunction also OK" $ [2,4,6,8] @=?+ observeMany 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ ((return 0 `mplus` return 1) >>-+ \a -> oddsPlus a) >>=+ (\x -> if even x then return x else mzero)+ )++ -- Here the application is effectively rewritten as+ --+ -- interleave (oddsPlus 0 >>- \x -> if ...)+ -- (oddsPlus 1 >>- \x -> if ...)+ --+ -- which fails to produce any values because interleave still+ -- requires production of values from both branches to switch+ -- between those values, but the first (oddsPlus 0 ...) never+ -- produces any values.++ , testCase "fair conjunction NON-PRODUCTIVE" $+ (Left () @=?) =<<+ (nonTerminating $+ observeManyT 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ (return 0 `mplus` return 1) >>-+ \a -> oddsPlus a >>-+ (\x -> if even x then return x else mzero)+ ))++ -- This shows that the second >>- is effectively >>= since+ -- there's no choice point for it, and values still cannot be+ -- produced.++ , testCase "fair conjunction also NON-PRODUCTIVE" $+ (Left () @=?) =<<+ (nonTerminating $+ observeManyT 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ (return 0 `mplus` return 1) >>-+ \a -> oddsPlus a >>=+ (\x -> if even x then return x else mzero)+ ))++ -- unfair conjunction does not terminate or produce any+ -- values: this will fail (expectedly) due to a timeout++ , testCase "unfair conjunction is NON-PRODUCTIVE" $+ (Left () @=?) =<<+ (nonTerminating $+ observeManyT 4 (let oddsPlus n = odds >>= \a -> return (a + n) in+ do x <- (return 0 `mplus` return 1) >>= oddsPlus+ if even x then return x else mzero+ ))++ , testCase "fair conjunction :: []" $ [2,4,6,8] @=?+ (take 4 $ let oddsL = [ 1 :: Integer ] `mplus` [ o | o <- [3..], odd o ]+ oddsPlus n = [ a + n | a <- oddsL ]+ in do x <- [0] `mplus` [1] >>- oddsPlus+ if even x then return x else mzero+ )++ , testCase "fair conjunction :: ReaderT" $ [2,4,6,8] @=?+ (take 4 $ runReaderT (let oddsR = return (1 :: Integer) `mplus` liftM (2+) oddsR+ oddsPlus n = oddsR >>= \a -> return (a + n)+ in do x <- (return 0 `mplus` return 1) >>- oddsPlus+ if even x then return x else mzero+ ) "env")++ , testCase "fair conjunction :: strict StateT" $ [2,4,6,8] @=?+ (take 4 $ SS.evalStateT (let oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS+ oddsPlus n = oddsS >>= \a -> return (a + n)+ in do x <- (return 0 `mplus` return 1) >>- oddsPlus+ if even x then return x else mzero+ ) "state")++ , testCase "fair conjunction :: lazy StateT" $ [2,4,6,8] @=?+ (take 4 $ SL.evalStateT (let oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS+ oddsPlus n = oddsS >>= \a -> return (a + n)+ in do x <- (return 0 `mplus` return 1) >>- oddsPlus+ if even x then return x else mzero+ ) "env")+ ]++ , testGroup "ifte logical conditional (soft-cut)"+ [+ -- Initial example returns all odds which are divisible by+ -- another number. Nothing special is needed to implement this.++ let iota n = msum (map return [1..n])+ oc = do n <- odds+ guard (n > 1)+ d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0)+ return n+ in testCase "divisible odds" $ [9,15,15,21,21,25,27,27,33,33] @=?+ observeMany 10 oc++ -- To get the inverse: all odds which are *not* divisible by+ -- another number, the guard test cannot simply be reversed:+ -- there are many produced values that are not divisors, but+ -- some that are:++ , let iota n = msum (map return [1..n])+ oc = do n <- odds+ guard (n > 1)+ d <- iota (n - 1)+ guard (d > 1 && n `mod` d /= 0)+ return n+ in testCase "indivisible odds, wrong" $+ [3,5,5,5,7,7,7,7,7,9] @=?+ observeMany 10 oc++ -- For the inverse logic to work correctly, it should return+ -- values only when there are *no* divisors at all. This can be+ -- done using the "soft cut" or "negation as finite failure" to+ -- needed to fail the current solution entirely. This is+ -- provided by logict as the 'ifte' operator.++ , let iota n = msum (map return [1..n])+ oc = do n <- odds+ guard (n > 1)+ ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: LogicT" $ [3,5,7,11,13,17,19,23,29,31] @=?+ observeMany 10 oc++ , let iota n = [1..n]+ oddsL = [ 1 :: Integer ] `mplus` [ o | o <- [3..], odd o ]+ oc = [ n+ | n <- oddsL+ , (n > 1)+ ] >>= \n -> ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: []" $ [3,5,7,11,13,17,19,23,29,31] @=?+ take 10 oc++ , let iota n = msum (map return [1..n])+ oddsR = return (1 :: Integer) `mplus` liftM (2+) oddsR+ oc = do n <- oddsR+ guard (n > 1)+ ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: ReaderT" $ [3,5,7,11,13,17,19,23,29,31] @=?+ (take 10 $ runReaderT oc "env")++ , let iota n = msum (map return [1..n])+ oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS+ oc = do n <- oddsS+ guard (n > 1)+ ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: strict StateT" $ [3,5,7,11,13,17,19,23,29,31] @=?+ (take 10 $ SS.evalStateT oc "state")++ , let iota n = msum (map return [1..n])+ oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS+ oc = do n <- oddsS+ guard (n > 1)+ ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: strict StateT" $ [3,5,7,11,13,17,19,23,29,31] @=?+ (take 10 $ SL.evalStateT oc "state")++ ]++ , testGroup "once (pruning)" $+ -- the pruning primitive 'once' selects (non-deterministically)+ -- a single candidate from many results and disables any further+ -- backtracking on this choice.++ let bogosort l = do p <- permute l+ if sorted p then return p else mzero++ sorted (e:e':r) = e <= e' && sorted (e':r)+ sorted _ = True++ permute [] = return []+ permute (h:t) = do { t' <- permute t; insert h t' }++ insert e [] = return [e]+ insert e l@(h:t) = return (e:l) `mplus`+ do { t' <- insert e t; return (h : t') }++ inp = [5,0,3,4,0,1 :: Integer]+ in+ [+ -- without pruning, get two results because 0 appears twice+ testCase "no pruning" $ [[0,0,1,3,4,5], [0,0,1,3,4,5]] @=?+ observeAll (bogosort inp)++ -- with pruning, stops after the first result+ , testCase "with pruning" $ [[0,0,1,3,4,5]] @=?+ observeAll (once (bogosort inp))+ ]+ ]++ , testGroup "lnot (inversion)" $+ let isEven n = if even n then return n else mzero in+ [+ testCase "inversion :: LogicT" $ [1,3,5,7,9] @=?+ observeMany 5 (do v <- foldr (mplus . return) mzero [(1::Integer)..]+ lnot (isEven v)+ return v)++ , testCase "inversion :: []" $ [1,3,5,7,9] @=?+ (take 5 $ do v <- [(1::Integer)..]+ lnot (isEven v)+ return v)++ , testCase "inversion :: ReaderT" $ [1,3,5,7,9] @=?+ (take 5 $ runReaderT (do v <- foldr (mplus . return) mzero [(1::Integer)..]+ lnot (isEven v)+ return v) "env")++ , testCase "inversion :: strict StateT" $ [1,3,5,7,9] @=?+ (take 5 $ SS.evalStateT (do v <- foldr (mplus . return) mzero [(1::Integer)..]+ lnot (isEven v)+ return v) "state")++ , testCase "inversion :: lazy StateT" $ [1,3,5,7,9] @=?+ (take 5 $ SL.evalStateT (do v <- foldr (mplus . return) mzero [(1::Integer)..]+ lnot (isEven v)+ return v) "state")+ ]+ ]++safely :: IO Integer -> IO (Either String Integer)+safely o = fmap (left (head . lines . show)) (try o :: IO (Either SomeException Integer))++-- | This is used to test logic operations that don't typically+-- terminate by running a parallel race between the operation and a+-- timer. A result of @Left ()@ means that the timer won and the+-- operation did not terminate within that time period.++nonTerminating :: IO a -> IO (Either () a)+nonTerminating op = race (threadDelay 100000) op -- returns Left () after 0.1s