diff --git a/Control/Monad/Logic.hs b/Control/Monad/Logic.hs --- a/Control/Monad/Logic.hs +++ b/Control/Monad/Logic.hs @@ -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 -- --- Adapted from the paper --- /Backtracking, Interleaving, and Terminating --- Monad Transformers/, by --- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry --- (). +-- Adapted from the paper +-- +-- 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 +-- or +-- +-- 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 +-- . +-- 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 +-- . +-- 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 +-- . +-- 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 +-- +-- 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 diff --git a/Control/Monad/Logic/Class.hs b/Control/Monad/Logic/Class.hs --- a/Control/Monad/Logic/Class.hs +++ b/Control/Monad/Logic/Class.hs @@ -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 -- --- Adapted from the paper --- /Backtracking, Interleaving, and Terminating --- Monad Transformers/, by --- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry --- () +-- Adapted from the paper +-- +-- 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 + -- ) + -- 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 + -- + -- (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 + -- . + -- 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) diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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: diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,125 @@ +# logict [![Build Status](https://github.com/Bodigrim/logict/workflows/Haskell-CI/badge.svg)](https://github.com/Bodigrim/logict/actions?query=workflow%3AHaskell-CI) [![Hackage](http://img.shields.io/hackage/v/logict.svg)](https://hackage.haskell.org/package/logict) [![Stackage LTS](http://stackage.org/package/logict/badge/lts)](http://stackage.org/lts/package/logict) [![Stackage Nightly](http://stackage.org/package/logict/badge/nightly)](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). diff --git a/changelog.md b/changelog.md new file mode 100644 --- /dev/null +++ b/changelog.md @@ -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. diff --git a/example/grandparents.hs b/example/grandparents.hs new file mode 100644 --- /dev/null +++ b/example/grandparents.hs @@ -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 diff --git a/logict.cabal b/logict.cabal --- a/logict.cabal +++ b/logict.cabal @@ -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: - -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 +author: Dan Doel +homepage: https://github.com/Bodigrim/logict#readme +synopsis: A backtracking logic-programming monad. +description: + Adapted from the paper + + 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 diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -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