logict-0.2.3: Control/Monad/Logic/Class.hs
-------------------------------------------------------------------------
-- |
-- Module : Control.Monad.Logic.Class
-- Copyright : (c) Dan Doel
-- License : BSD3
--
-- Maintainer : dan.doel@gmail.com
-- Stability : experimental
-- Portability : non-portable (multi-parameter type classes)
--
-- A backtracking, logic programming monad.
--
-- Adapted from the paper
-- /Backtracking, Interleaving, and Terminating
-- Monad Transformers/, by
-- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry
-- (<http://www.cs.rutgers.edu/~ccshan/logicprog/LogicT-icfp2005.pdf>)
-------------------------------------------------------------------------
module Control.Monad.Logic.Class (MonadLogic(..), reflect) where
import qualified Control.Monad.State.Lazy as LazyST
import qualified Control.Monad.State.Strict as StrictST
import Control.Monad.Reader
import Data.Monoid
import qualified Control.Monad.Writer.Lazy as LazyWT
import qualified Control.Monad.Writer.Strict as StrictWT
-------------------------------------------------------------------------------
-- | Minimal implementation: msplit
class (MonadPlus 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 :: m a -> m (Maybe (a, m a))
-- | 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
--
-- Such computations can cause problems in some circumstances. Consider:
--
-- > do x <- odds `mplus` return 2
-- > if even x then return x else mzero
--
-- 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
interleave :: m a -> m a -> m a
-- | Fair conjunction. Similarly to the previous function, consider
-- the distributivity law for MonadPlus:
--
-- > (mplus a b) >>= k = (a >>= k) `mplus` (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:
--
-- > ifte (return a) th el == th a
-- > ifte mzero th el == el
-- > ifte (return a `mplus` m) th el == th a `mplus` (m >>= th)
ifte :: m a -> (a -> m b) -> m b -> m b
-- | Pruning. Selects one result out of many. Useful for when multiple
-- results of a computation will be equivalent, or should be treated as
-- such.
once :: m a -> m a
-- 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')
m >>- f = do Just (a, m') <- msplit m
interleave (f a) (m' >>- f)
ifte t th el = msplit t >>= maybe el (\(a,m) -> th a `mplus` (m >>= th))
once m = do Just (a, _) <- msplit m
return a
-------------------------------------------------------------------------------
-- | 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
-- An instance of MonadLogic for lists
instance MonadLogic [] where
msplit [] = return Nothing
msplit (x:xs) = return $ 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:
--
-- 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.
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))
instance (MonadLogic 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)
Just ((a,s'), m) ->
return (Just (a, StrictST.StateT (\_ -> m)), s')
interleave ma mb = StrictST.StateT $ \s ->
StrictST.runStateT ma s `interleave` StrictST.runStateT mb s
ma >>- f = StrictST.StateT $ \s ->
StrictST.runStateT ma s >>- \(a,s') -> StrictST.runStateT (f a) s'
ifte t th el = StrictST.StateT $ \s -> ifte (StrictST.runStateT t s)
(\(a,s') -> StrictST.runStateT (th a) s')
(StrictST.runStateT el s)
once ma = StrictST.StateT $ \s -> once (StrictST.runStateT ma s)
instance (MonadLogic 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)
Just ((a,s'), m) ->
return (Just (a, LazyST.StateT (\_ -> m)), s')
interleave ma mb = LazyST.StateT $ \s ->
LazyST.runStateT ma s `interleave` LazyST.runStateT mb s
ma >>- f = LazyST.StateT $ \s ->
LazyST.runStateT ma s >>- \(a,s') -> LazyST.runStateT (f a) s'
ifte t th el = LazyST.StateT $ \s -> ifte (LazyST.runStateT t s)
(\(a,s') -> LazyST.runStateT (th a) s')
(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)