logict 0.5.0.2 → 0.8.2.0
raw patch · 8 files changed
Files
- Control/Monad/Logic.hs +511/−60
- Control/Monad/Logic/Class.hs +368/−125
- LICENSE +6/−1
- README.md +125/−0
- changelog.md +49/−0
- example/grandparents.hs +23/−0
- logict.cabal +68/−27
- test/Test.hs +601/−0
Control/Monad/Logic.hs view
@@ -1,24 +1,36 @@-{-# LANGUAGE UndecidableInstances, Rank2Types, FlexibleInstances, MultiParamTypeClasses #-}- ------------------------------------------------------------------------- -- | -- 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 : dan.doel@gmail.com--- Stability : experimental--- Portability : non-portable (multi-parameter type classes)------ A backtracking, logic programming monad.+-- Maintainer : Andrew Lelechenko <andrew.lelechenko@gmail.com> ----- Adapted from the paper--- /Backtracking, Interleaving, and Terminating--- Monad Transformers/, by--- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry--- (<http://www.cs.rutgers.edu/~ccshan/logicprog/LogicT-icfp2005.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+-- ('Control.Monad.mzero' and 'Control.Monad.mplus'),+-- while examples below prefer 'empty' and '<|>'+-- from 'Alternative'. ------------------------------------------------------------------------- +{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Avoid restricted function" #-}+ module Control.Monad.Logic ( module Control.Monad.Logic.Class, -- * The Logic monad@@ -34,90 +46,361 @@ observeT, observeManyT, observeAllT,- module Control.Monad,- module Control.Monad.Trans+ fromLogicT,+ fromLogicTWith,+ hoistLogicT,+ embedLogicT ) where -import Control.Applicative--import Control.Monad-import Control.Monad.Identity-import Control.Monad.Trans+import Prelude (error, (-)) -import Control.Monad.Reader.Class-import Control.Monad.State.Class-import Control.Monad.Error.Class+import Control.Applicative (Alternative(..), Applicative, liftA2, pure, (<*>), (*>))+import Control.Exception (Exception, evaluate, throw)+import Control.Monad (join, MonadPlus(..), Monad(..), fail)+import Control.Monad.Catch (MonadThrow, MonadCatch, throwM, catch)+import Control.Monad.Error.Class (MonadError(..))+import qualified Control.Monad.Fail as Fail+import Control.Monad.Identity (Identity(..))+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Reader.Class (MonadReader(..))+import Control.Monad.State.Class (MonadState(..))+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.Zip (MonadZip (..)) -import Data.Monoid (Monoid(mappend, mempty))+import Data.Bool (Bool (..), otherwise)+import Data.Eq (Eq, (==)) import qualified Data.Foldable as F+import Data.Function (($), (.), const, on)+import Data.Functor (Functor(..), (<$>))+import Data.Int+import qualified Data.List as L+import Data.Maybe (Maybe(..), maybe)+import Data.Monoid (Monoid (..))+import Data.Ord (Ord, (<=), (>), compare)+import Data.Semigroup (Semigroup (..)) import qualified Data.Traversable as T+import System.IO.Unsafe (unsafePerformIO)+import Text.Show (Show, showsPrec, showParen, showString, shows)+import Text.Read (Read, readPrec, Lexeme (Ident), parens, lexP, prec, readListPrec, readListPrecDefault) +#if MIN_VERSION_base(4,17,0)+import GHC.IsList (IsList(..))+#else+import GHC.Exts (IsList(..))+#endif++#if MIN_VERSION_base(4,18,0)+import qualified Data.Foldable1 as F1+#endif+ import Control.Monad.Logic.Class ------------------------------------------------------------------------- -- | A monad transformer for performing backtracking computations--- layered over another monad 'm'+-- 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.+--+-- It's important to remember that 'LogicT' on its own is just+-- a lawful list monad transformer, adding a nondeterministic effect,+-- and its 'Monad' instance behaves just as @instance@ 'Monad' @[]@:+--+-- >>> :set -XOverloadedLists+-- >>> observeMany 9 $ do {x <- [100,200] :: Logic Int; fmap (+x) [1..]}+-- [101,102,103,104,105,106,107,108,109]+-- >>> observeMany 9 $ do {[100,200] >>= \x -> fmap (+x) [1..] :: Logic Int}+-- [101,102,103,104,105,106,107,108,109]+--+-- One should explicitly use methods of 'MonadLogic' such as '(>>-)' and 'interleave'+-- to get fair conjunction / disjunction:+--+-- >>> observeMany 9 $ do {[100,200] >>- \x -> fmap (+x) [1..] :: Logic Int}+-- [101,201,102,202,103,203,104,204,105]+--+-- @since 0.2 newtype LogicT m a = 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.+--+-- @since 0.2+#if !MIN_VERSION_base(4,13,0) observeT :: Monad m => LogicT m a -> m a+#else+observeT :: Fail.MonadFail m => LogicT m a -> m a+#endif 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.+--+-- @since 0.2+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.+--+-- @since 0.2 observeManyT :: Monad m => Int -> LogicT m a -> m [a] observeManyT n m | n <= 0 = return [] | n == 1 = unLogicT m (\a _ -> return [a]) (return []) | otherwise = unLogicT (msplit m) sk (return [])- where- sk Nothing _ = return []- sk (Just (a, m')) _ = (a:) `liftM` observeManyT (n-1) m'+ where+ sk Nothing _ = return []+ sk (Just (a, m')) _ = (a:) <$> 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+--+-- @since 0.2 runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r-runLogicT = unLogicT+runLogicT (LogicT r) = r +-- | Convert from 'LogicT' to an arbitrary logic-like monad transformer,+-- such as <https://hackage.haskell.org/package/list-t list-t>+-- or <https://hackage.haskell.org/package/logict-sequence 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)+--+-- 'Text.Show.show' $ fromLogicT @ListT l+-- @+--+-- @since 0.8.0.0+fromLogicT :: (Alternative (t m), MonadTrans t, Monad m, Monad (t m))+ => LogicT m a -> t m a+fromLogicT = fromLogicTWith lift++-- | 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+-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.+-- to produce sensible results.+--+-- @since 0.8.0.0+fromLogicTWith :: (Applicative m, Monad n, Alternative n)+ => (forall x. m x -> n x) -> LogicT m a -> n a+fromLogicTWith p (LogicT f) = join . p $+ f (\a v -> pure (pure a <|> join (p v))) (pure empty)++-- | 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+-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html 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+hoistLogicT f = fromLogicTWith (lift . f)++-- | Convert a 'LogicT' computation from one underlying monad to another.+--+-- The first argument should be a+-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html 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+embedLogicT f = fromLogicTWith f+ ---------------------------------------------------------------------------- | 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@).+--+-- It's important to remember that 'Logic' on its own is just+-- a lawful list monad, behaving exactly as @instance@ 'Monad' @[]@.+-- One should explicitly use methods of 'MonadLogic' such as '(>>-)' and 'interleave'+-- to get fair conjunction / disjunction. Note that usual+-- lists have an instance of 'MonadLogic', so maybe you don't need 'Logic' at all.+--+-- __Technical perspective.__+-- 'Logic' is a+-- <http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Boehm-Berarducci encoding>+-- of lists. Speaking plainly, its type is identical (up to 'Identity' wrappers)+-- to 'Data.List.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 type Logic = LogicT Identity ---------------------------------------------------------------------------- | A smart constructor for Logic computations.+-- | A smart constructor for 'Logic' computations.+--+-- @since 0.5.0 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.+--+-- Since 'Logic' is isomorphic to a list, 'observe' is analogous to 'Data.List.head'.+--+-- @since 0.2 observe :: Logic a -> a-observe = runIdentity . observeT +observe lt = runIdentity $ unLogicT lt (const . pure) (error "No answer.") ---------------------------------------------------------------------------- | Extracts all results from a Logic computation.+-- | 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 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]+--+-- Since 'Logic' is isomorphic to a list, 'observeMany' is analogous to 'Data.List.take'.+--+-- @since 0.2 observeMany :: Int -> Logic a -> [a]-observeMany i = runIdentity . observeManyT i+observeMany i = L.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+--+-- 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 runLogic :: Logic a -> (a -> r -> r) -> r -> r runLogic l s f = runIdentity $ unLogicT l si fi where@@ -130,51 +413,219 @@ instance Applicative (LogicT f) where pure a = LogicT $ \sk fk -> sk a fk f <*> a = LogicT $ \sk fk -> unLogicT f (\g fk' -> unLogicT a (sk . g) fk') fk+ m *> k = LogicT $ \sk fk -> unLogicT m (const $ unLogicT k sk) fk instance Alternative (LogicT f) where empty = LogicT $ \_ fk -> fk 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+#endif++-- | @since 0.6.0.3+instance Fail.MonadFail (LogicT m) where 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 = (<|>) +-- | @since 0.7.0.3+instance Semigroup (LogicT m a) where+ (<>) = mplus+#if MIN_VERSION_base(4,18,0)+ sconcat = F1.foldr1 mplus+#else+ sconcat = F.foldr1 mplus+#endif++-- | @since 0.7.0.3+instance Monoid (LogicT m a) where+ mempty = empty+ mappend = (<>)+ mconcat = F.asum+ instance MonadTrans LogicT where lift m = LogicT $ \sk fk -> m >>= \a -> sk a fk instance (MonadIO m) => MonadIO (LogicT m) where liftIO = lift . liftIO -instance (Monad m) => MonadLogic (LogicT m) where+instance {-# OVERLAPPABLE #-} (Monad m) => MonadLogic (LogicT m) where+ -- 'msplit' is quite costly even if the base 'Monad' is 'Identity'.+ -- 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) -instance (Monad m, F.Foldable m) => F.Foldable (LogicT m) where- foldMap f m = F.fold $ unLogicT m (liftM . mappend . f) (return mempty)+-- | @since 0.8.2.0+instance {-# INCOHERENT #-} MonadLogic Logic where+ -- Same as in the generic instance above+ msplit m = lift $ unLogicT m ssk (return Nothing)+ where+ 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) -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'+ m >>- f+ | isConstantFailure f = empty+ -- Otherwise apply the default definition from Control.Monad.Logic.Class+ | otherwise = msplit m >>= maybe empty (\(a, m') -> interleave (f a) (m' >>- f)) --- Needs undecidable instances+data MyException = MyException+ deriving (Show)++instance Exception MyException++isConstantFailure :: (a -> Logic b) -> Bool+isConstantFailure f = unsafePerformIO $ do+ let eval foo = runIdentity (unLogicT foo (const $ const $ Identity False) (Identity True))+ evaluate (eval (f (throw MyException))) `catch` (\MyException -> pure False)++-- | @since 0.5.0+instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where+ foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty)++-- | @since 0.5.0+instance {-# INCOHERENT #-} F.Foldable Logic where+ foldr f z m = runLogic m f z++-- A much simpler logic monad representation used to define the Traversable and+-- MonadZip instances. This is essentially the same as ListT from the list-t+-- package, but it uses a slightly more efficient representation: MLView m a is+-- more compact than Maybe (a, ML m a), and the additional laziness in the+-- latter appears to be incidental/historical.+newtype ML m a = ML (m (MLView m a))+ deriving (Functor, F.Foldable, T.Traversable)++data MLView m a = EmptyML | ConsML a (ML m a)+ deriving (Functor, F.Foldable)++instance T.Traversable m => T.Traversable (MLView m) where+ traverse _ EmptyML = pure EmptyML+ traverse f (ConsML x (ML m))+ = liftA2 (\y ym -> ConsML y (ML ym)) (f x) (T.traverse (T.traverse f) m)+ {- The derived instance would write the second case as+ -+ - traverse f (ConsML x xs) = liftA2 ConsML (f x) (traverse @(ML m) f xs)+ -+ - Inlining the inner traverse gives+ -+ - traverse f (ConsML x (ML m)) = liftA2 ConsML (f x) (ML <$> traverse (traverse f) m)+ -+ - revealing fmap under liftA2. We fuse those into a single application of liftA2,+ - in case fmap isn't free.+ -}++toML :: Applicative m => LogicT m a -> ML m a+toML (LogicT q) = ML $ q (\a m -> pure $ ConsML a (ML m)) (pure EmptyML)++fromML :: Monad m => ML m a -> LogicT m a+fromML (ML m) = lift m >>= \case+ EmptyML -> empty+ ConsML a xs -> pure a <|> fromML xs++-- | @since 0.5.0+instance {-# OVERLAPPING #-} T.Traversable (LogicT Identity) where+ traverse g l = runLogic l (\a ft -> cons <$> g a <*> ft) (pure empty)+ where+ cons a l' = pure a <|> l'++-- | @since 0.8.0.0+instance {-# OVERLAPPABLE #-} (Monad m, T.Traversable m) => T.Traversable (LogicT m) where+ traverse f = fmap fromML . T.traverse f . toML++zipWithML :: MonadZip m => (a -> b -> c) -> ML m a -> ML m b -> ML m c+zipWithML f = go+ where+ go (ML m1) (ML m2) =+ ML $ mzipWith zv m1 m2+ zv (a `ConsML` as) (b `ConsML` bs) = f a b `ConsML` go as bs+ zv _ _ = EmptyML++unzipML :: MonadZip m => ML m (a, b) -> (ML m a, ML m b)+unzipML (ML m)+ | (l, r) <- munzip (fmap go m)+ = (ML l, ML r)+ where+ go EmptyML = (EmptyML, EmptyML)+ go ((a, b) `ConsML` listab)+ = (a `ConsML` la, b `ConsML` lb)+ where+ -- If the underlying munzip is careful not to leak memory, then we+ -- don't want to defeat it. We need to be sure that la and lb are+ -- realized as selector thunks. Hopefully the CPSish conversion+ -- doesn't muck anything up at another level.+ {-# NOINLINE remains #-}+ {-# NOINLINE la #-}+ {-# NOINLINE lb #-}+ remains = unzipML listab+ (la, lb) = remains++-- | @since 0.8.0.0+instance MonadZip m => MonadZip (LogicT m) where+ mzipWith f xs ys = fromML $ zipWithML f (toML xs) (toML ys)+ munzip xys = case unzipML (toML xys) of+ (xs, ys) -> (fromML xs, fromML ys)+ instance MonadReader r m => MonadReader r (LogicT m) where ask = lift ask- local f m = LogicT $ \sk fk -> unLogicT m ((local f .) . sk) (local f fk)+ local f (LogicT m) = LogicT $ \sk fk -> do+ env <- ask+ local f $ m ((local (const env) .) . sk) (local (const env) fk) --- Needs undecidable instances instance MonadState s m => MonadState s (LogicT m) where get = lift get put = lift . put --- Needs undecidable instances+-- | @since 0.4 instance MonadError e m => MonadError e (LogicT m) where throwError = lift . throwError catchError m h = LogicT $ \sk fk -> let handle r = r `catchError` \e -> unLogicT (h e) sk fk in handle $ unLogicT m (\a -> sk a . handle) fk++-- | @since 0.8.2.0+instance MonadThrow m => MonadThrow (LogicT m) where+ throwM = lift . throwM++-- | @since 0.8.2.0+instance MonadCatch m => MonadCatch (LogicT m) where+ catch m h = LogicT $ \sk fk -> let+ handle r = r `catch` \e -> unLogicT (h e) sk fk+ in handle $ unLogicT m (\a -> sk a . handle) fk++-- | @since 0.8.2.0+instance IsList (Logic a) where+ type Item (Logic a) = a+ fromList xs = LogicT $ \cons nil -> L.foldr cons nil xs+ toList = observeAll++-- | @since 0.8.2.0+instance Eq a => Eq (Logic a) where+ (==) = (==) `on` observeAll++-- | @since 0.8.2.0+instance Ord a => Ord (Logic a) where+ compare = compare `on` observeAll++-- | @since 0.8.2.0+instance Show a => Show (Logic a) where+ showsPrec p xs = showParen (p > 10) $+ showString "fromList " . shows (toList xs)++-- | @since 0.8.2.0+instance Read a => Read (Logic a) where+ readPrec = parens $ prec 10 $ do+ Ident "fromList" <- lexP+ xs <- readPrec+ return (fromList xs)++ readListPrec = readListPrecDefault
Control/Monad/Logic/Class.hs view
@@ -1,138 +1,424 @@ ------------------------------------------------------------------------- -- | -- 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 : dan.doel@gmail.com--- Stability : experimental--- Portability : non-portable (multi-parameter type classes)------ A backtracking, logic programming monad.+-- Maintainer : Andrew Lelechenko <andrew.lelechenko@gmail.com> ----- Adapted from the paper--- /Backtracking, Interleaving, and Terminating--- Monad Transformers/, by--- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry--- (<http://www.cs.rutgers.edu/~ccshan/logicprog/LogicT-icfp2005.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+-- ('Control.Monad.mzero' and 'Control.Monad.mplus'),+-- while examples below prefer 'empty' and '<|>'+-- from 'Alternative'. ------------------------------------------------------------------------- -module Control.Monad.Logic.Class (MonadLogic(..), reflect, lnot) where+{-# LANGUAGE CPP #-}+{-# LANGUAGE Trustworthy #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Avoid restricted function" #-}++module Control.Monad.Logic.Class (MonadLogic(..), reflect) where++import Prelude ()++import Control.Applicative (Alternative(..), Applicative(..))+import Control.Exception (Exception, evaluate, catch, throw)+import Control.Monad (MonadPlus, 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--import Control.Monad.Reader+import Data.Bool (Bool(..), otherwise)+import Data.Function (const, ($))+import Data.List (null)+import Data.Maybe (Maybe(..), maybe)+import System.IO.Unsafe (unsafePerformIO)+import Text.Show (Show) +#if MIN_VERSION_mtl(2,3,0)+import qualified Control.Monad.Writer.CPS as CpsW+import qualified Control.Monad.Trans.Writer.CPS as CpsW (writerT, runWriterT) import Data.Monoid-import qualified Control.Monad.Writer.Lazy as LazyWT-import qualified Control.Monad.Writer.Strict as StrictWT+#endif ----------------------------------------------------------------------------------- | Minimal implementation: msplit-class (MonadPlus m) => MonadLogic m where- -- | Attempts to split the computation, giving access to the first+-- | A backtracking, logic programming monad.+--+-- This package offers one implementation of 'MonadLogic': 'Control.Monad.Logic.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+--+-- @since 0.2+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.- (>>-) :: m a -> (a -> m b) -> m b-- -- | 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:+ -- 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: --- -- > 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+ -- >>> 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@ or @QualifiedDo@ language pragmas cannot easily be used+ -- either. Instead, it is recommended to carefully use explicit+ -- '>>-' only when needed.+ --+ -- Here is an action of '(>>-)' on lists:+ --+ -- >>> 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..]@ 'interleave'd+ -- 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!+ --+ (>>-) :: m a -> (a -> m b) -> m b+ infixl 1 >>- - -- | 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 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.+ --+ -- @since 0.7.0.0+ 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 'Data.Bool.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))+ --+ -- >>> 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 Just (a, m') <- msplit m- interleave (f a) (m' >>- f)+ m >>- f = msplit m >>= maybe empty+ (\(a, 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 Just (a, _) <- msplit m- return a+ once m = msplit m >>= maybe empty (\(a, _) -> pure a) + lnot m = msplit m >>= maybe (pure ()) (const empty)+ ---------------------------------------------------------------------------------- | 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---- | Inverts a logic computation. If @m@ succeeds with at least one value,--- @lnot m@ fails. If @m@ fails, then @lnot m@ succeeds the value @()@.-lnot :: MonadLogic m => m a -> m ()-lnot m = ifte (once m) (const mzero) (return ())+--+-- @since 0.2+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) --- Some of these may be questionable instances. Splitting a transformer does--- not allow you to provide different input to the monadic object returned.--- So, for instance, in:+ m >>- f+ | isConstantFailure f = []+ -- Otherwise apply the default definition+ | otherwise = msplit m >>= maybe empty (\(a, m') -> interleave (f a) (m' >>- f))++data MyException = MyException+ deriving (Show)++instance Exception MyException++isConstantFailure :: (a -> [b]) -> Bool+isConstantFailure f = unsafePerformIO $+ evaluate (null (f (throw MyException))) `catch` (\MyException -> pure False)++-- | Note 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'+-- > let Just (_, rm') = runReaderT (msplit rm) r in runReaderT rm' r' ----- The "r'" parameter will be ignored, as "r" was already threaded through the--- computation. The results are similar for StateT. However, this is likely not--- an issue as most uses of msplit (all the ones in this library, at least) would--- not allow for that anyway.+-- @r'@ will be ignored, because @r@ was already threaded through the+-- computation. 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)) -instance MonadLogic m => MonadLogic (StrictST.StateT s m) where+#if MIN_VERSION_mtl(2,3,0)+-- | @since 0.8.1.0+instance (Monoid w, MonadLogic m, MonadPlus m) => MonadLogic (CpsW.WriterT w m) where+ msplit wm = CpsW.writerT $ do+ r <- msplit $ CpsW.runWriterT wm+ case r of+ Nothing -> pure (Nothing, mempty)+ Just ((a, w), m) -> pure (Just (a, CpsW.writerT m), w)+#endif++-- | See note on splitting above.+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 +432,14 @@ once ma = StrictST.StateT $ \s -> once (StrictST.runStateT ma s) -instance MonadLogic m => MonadLogic (LazyST.StateT s m) where+-- | See note on splitting above.+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@@ -165,47 +452,3 @@ (LazyST.runStateT el s) once ma = LazyST.StateT $ \s -> once (LazyST.runStateT ma s)--instance (MonadLogic m, Monoid w) => MonadLogic (StrictWT.WriterT w m) where- msplit wm = StrictWT.WriterT $- do r <- msplit (StrictWT.runWriterT wm)- case r of- Nothing -> return (Nothing, mempty)- Just ((a,w), m) ->- return (Just (a, StrictWT.WriterT m), w)-- interleave ma mb = StrictWT.WriterT $- StrictWT.runWriterT ma `interleave` StrictWT.runWriterT mb-- ma >>- f = StrictWT.WriterT $- StrictWT.runWriterT ma >>- \(a,w) ->- StrictWT.runWriterT (StrictWT.tell w >> f a)-- ifte t th el = StrictWT.WriterT $- ifte (StrictWT.runWriterT t)- (\(a,w) -> StrictWT.runWriterT (StrictWT.tell w >> th a))- (StrictWT.runWriterT el)-- once ma = StrictWT.WriterT $ once (StrictWT.runWriterT ma)--instance (MonadLogic m, Monoid w) => MonadLogic (LazyWT.WriterT w m) where- msplit wm = LazyWT.WriterT $- do r <- msplit (LazyWT.runWriterT wm)- case r of- Nothing -> return (Nothing, mempty)- Just ((a,w), m) ->- return (Just (a, LazyWT.WriterT m), w)-- interleave ma mb = LazyWT.WriterT $- LazyWT.runWriterT ma `interleave` LazyWT.runWriterT mb-- ma >>- f = LazyWT.WriterT $- LazyWT.runWriterT ma >>- \(a,w) ->- LazyWT.runWriterT (LazyWT.tell w >> f a)-- ifte t th el = LazyWT.WriterT $- ifte (LazyWT.runWriterT t)- (\(a,w) -> LazyWT.runWriterT (LazyWT.tell w >> th a))- (LazyWT.runWriterT el)-- once ma = LazyWT.WriterT $ once (LazyWT.runWriterT ma)
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
@@ -0,0 +1,49 @@+# 0.8.2.0++* Add instances for `MonadThrow` and `MonadCatch`.+* Add instances `Eq`, `Ord`, `Show`, `Read`, `IsList` for `Logic a`.+* Speed up `instance MonadLogic Logic` with a trick to determine whether a callback is a constant failure.++# 0.8.1.0++* Add `instance MonadLogic (Control.Monad.Writer.CPS.WriterT w m)`.++# 0.8.0.0++* Breaking change:+ do not re-export `Control.Monad` and `Control.Monad.Trans` from `Control.Monad.Logic`.+* Generalize `instance Traversable (LogicT Identity)`+ to `instance (Traversable m, Monad m) => Traversable (LogicT m)`.+* Add conversion functions `fromLogicT` and `fromLogicTWith` to facilitate+ interoperation with [`list-t`](https://hackage.haskell.org/package/list-t)+ and [`logict-sequence`](https://hackage.haskell.org/package/logict-sequence) packages.+* Add `hoistLogicT` and `embedLogicT` to convert `LogicT` computations+ from one underlying monad to another.++# 0.7.1.0++* Improve documentation.+* Breaking change:+ relax superclasses of `MonadLogic` to `Monad` and `Alternative` instead of `MonadPlus`.++# 0.7.0.3++* Support GHC 9.0.++# 0.7.0.2++* Add `Safe` pragmas.++# 0.7.0.1++* Fix `MonadReader r (LogicT m)` instance again.++# 0.7.0.0++* Remove unlawful `MonadLogic (Writer T w m)` instances.+* Fix `MonadReader r (LogicT m)` instance.+* Move `lnot` into `MonadLogic` class.++# 0.6.0.3++* Comply with MonadFail proposal.
+ example/grandparents.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE CPP #-}++import Control.Applicative+import Control.Monad.Logic+import Data.Semigroup (Semigroup (..))++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,29 +1,70 @@-Name: logict-Version: 0.5.0.2-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>-Synopsis: A backtracking logic-programming monad.-Category: Control-License: BSD3-License-File: LICENSE-Copyright: Copyright (c) 2007-2010, Dan Doel,- Copyright (c) 2011, Edward Kmett-Author: Dan Doel-Maintainer: dan.doel@gmail.com-Homepage: http://code.haskell.org/~dolio/logict+name: logict+version: 0.8.2.0+license: BSD3+license-file: LICENSE+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+maintainer: Andrew Lelechenko <andrew.lelechenko@gmail.com>+author: Dan Doel+homepage: https://github.com/Bodigrim/logict#readme+synopsis: A backtracking logic-programming monad.+description:+ 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 ==8.0.2 GHC ==8.2.2 GHC ==8.4.4 GHC ==8.6.5 GHC ==8.8.4 GHC ==8.10.7 GHC ==9.0.2 GHC ==9.2.8 GHC ==9.4.8 GHC ==9.6.6 GHC ==9.8.2 GHC ==9.10.1 GHC ==9.12.1 -Stability: Experimental-Tested-With: GHC-Build-Depends: base >=2 && < 5, mtl>=1.0.1 && <2.3-Build-Type: Simple+source-repository head+ type: git+ location: https://github.com/Bodigrim/logict -Exposed-Modules: Control.Monad.Logic,- Control.Monad.Logic.Class-Extensions: MultiParamTypeClasses,- UndecidableInstances,- Rank2Types,- FlexibleInstances-GHC-Options: -O2 -Wall+library+ exposed-modules:+ Control.Monad.Logic+ Control.Monad.Logic.Class+ default-language: Haskell2010++ ghc-options: -O2 -Wall -Wcompat++ build-depends:+ base >=4.9 && <5,+ mtl >=2.0 && <2.4,+ transformers <0.7,+ exceptions <0.11++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 -Wcompat -Wno-incomplete-uni-patterns++ build-depends:+ base,+ async >=2.0 && <2.3,+ logict,+ mtl,+ transformers,+ tasty <1.6,+ tasty-hunit <0.11++ hs-source-dirs: test
+ test/Test.hs view
@@ -0,0 +1,601 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Test.Tasty+import Test.Tasty.HUnit++import Control.Concurrent ( threadDelay )+import Control.Concurrent.Async ( race )+import Control.Exception+import Control.Monad+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.List (uncons)+import Data.Maybe++#if MIN_VERSION_base(4,17,0)+import GHC.IsList (IsList(..))+#else+import GHC.Exts (IsList(..))+#endif++#if !MIN_VERSION_base(4,11,0)+import Data.Semigroup (Semigroup (..))+#endif++#if MIN_VERSION_mtl(2,3,0)+import qualified Control.Monad.Writer.CPS as CpsW (WriterT, execWriterT, tell)+import qualified Control.Monad.Trans.Writer.CPS as CpsW (runWriterT)+import Data.Monoid+#endif++monadReader1 :: Assertion+monadReader1 = assertEqual "should be equal" [5 :: Int] $+ runReader (observeAllT (local (+ 5) ask)) 0++monadReader2 :: Assertion+monadReader2 = assertEqual "should be equal" [(5, 0)] $+ runReader (observeAllT foo) 0+ where+ foo :: MonadReader Int m => m (Int,Int)+ foo = do+ x <- local (5+) ask+ 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++-- | A `WriterT` version of `evalStateT`.+#if MIN_VERSION_mtl(2,3,0)+evalWriterT :: (Monad m, Monoid w) => CpsW.WriterT w m a -> m a+evalWriterT = fmap fst . CpsW.runWriterT+#endif++nats = pure 0 `mplus` ((1 +) <$> nats)++odds = return 1 `mplus` fmap (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 $+ localOption (mkTimeout 3000000) $ -- 3 second deadman timeout+ 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++ , testCase "(>>-) Logic" $ do+ let sample = fromList [1, 2, 3] :: Logic Integer+ (sample >>- const (mempty :: Logic Integer)) @?= mempty+ (sample >>- (\x -> fmap (+ x) (fromList [100, 200, 300]))) @?= fromList [101,102,201,103,301,202,203,302,303]+ (sample >>- (\x -> if odd x then fmap (+ x) (fromList [100, 200, 300]) else mempty)) @?= fromList [101,103,201,203,301,303]+ ]++ --------------------------------------------------++ , 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++#if MIN_VERSION_mtl(2,3,0)+ , testCase "msplit mzero :: CPS WriterT" $+ let z :: CpsW.WriterT (Sum Int) [] String+ z = mzero+ in assertBool "CPS WriterT" $ null $ catMaybes (evalWriterT (msplit z))+#endif++ , testCase "msplit mzero :: LogicT" $+ let z :: LogicT [] String+ z = mzero+ in assertBool "LogicT" $ all (null . catMaybes) $ 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 "(>>-) []" $ do+ (sample >>- const ([] :: [Integer])) @?= []+ (sample >>- (\x -> fmap (+ x) [100, 200, 300])) @?= [101,102,201,103,301,202,203,302,303]+ (sample >>- (\x -> if odd x then fmap (+ x) [100, 200, 300] else [])) @?= [101,103,201,203,301,303]++ , 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)) @?= []++#if MIN_VERSION_mtl(2,3,0)+ , testCase "msplit CPS WriterT" $ do+ let op :: CpsW.WriterT (Sum Integer) [] ()+ op = CpsW.tell 1 `mplus` op+ extract = CpsW.execWriterT+ extract (msplit op) @?= [1]+ extract (msplit op >>= \(Just (_,nxt)) -> msplit nxt) @?= [2]+#endif++ , testCase "msplit LogicT" $ do+ let op :: LogicT [] Integer+ op = foldr (mplus . return) mzero sample+ extract = fmap fst . concatMap catMaybes . 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` fmap (2+) oddsR+ in oddsR `interleave` return (2 :: Integer)) "go")++#if MIN_VERSION_mtl(2,3,0)+ , testCase "fair disjunction :: CPS WriterT" $ [1,2,3,5] @=?+ (take 4 $ evalWriterT (let oddsW :: CpsW.WriterT [Char] [] Integer+ oddsW = return 1 `mplus` fmap (2+) oddsW+ in oddsW `interleave` return (2 :: Integer)))+#endif++ , testCase "fair disjunction :: strict StateT" $ [1,2,3,5] @=?+ (take 4 $ SS.evalStateT (let oddsS = return 1 `mplus` fmap (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` fmap (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) >>-+ (oddsPlus >=>+ (\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` fmap (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")++#if MIN_VERSION_mtl(2,3,0)+ , testCase "fair conjunction :: CPS WriterT" $ [2,4,6,8] @=?+ (take 4 $ evalWriterT $+ (let oddsW :: CpsW.WriterT [Char] [] Integer+ oddsW = return (1 :: Integer) `mplus` fmap (2+) oddsW+ oddsPlus n = oddsW >>= \a -> return (a + n)+ in do x <- (return 0 `mplus` return 1) >>- oddsPlus+ if even x then return x else mzero+ ))+#endif++ , testCase "fair conjunction :: strict StateT" $ [2,4,6,8] @=?+ (take 4 $ SS.evalStateT (let oddsS = return (1 :: Integer) `mplus` fmap (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` fmap (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` fmap (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")++#if MIN_VERSION_mtl(2,3,0)+ , let iota n = msum (map return [1..n])+ oddsW = return (1 :: Integer) `mplus` fmap (2+) oddsW+ oc :: CpsW.WriterT [Char] [] Integer+ oc = do n <- oddsW+ guard (n > 1)+ ifte (do d <- iota (n - 1)+ guard (d > 1 && n `mod` d == 0))+ (const mzero)+ (return n)+ in testCase "indivisible odds :: CPS WriterT" $ [3,5,7,11,13,17,19,23,29,31] @=?+ (take 10 $ (fmap fst . CpsW.runWriterT) oc)+#endif++ , let iota n = msum (map return [1..n])+ oddsS = return (1 :: Integer) `mplus` fmap (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` fmap (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")++#if MIN_VERSION_mtl(2,3,0)+ , testCase "inversion :: CPS WriterT" $ [1,3,5,7,9] @=?+ (take 5 $ (evalWriterT :: CpsW.WriterT [Char] [] Integer -> [Integer])+ (do v <- foldr (mplus . return) mzero [(1::Integer)..]+ lnot (isEven v)+ return v))+#endif++ , 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 = do+ p <- try o+ pure $ case p of+ Left (err :: SomeException) -> Left $ maybe "" fst $ uncons $ lines $ show err+ Right n -> Right n++-- | 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