logict (empty) → 0.2

raw patch · 5 files changed

+394/−0 lines, 5 filesdep +basedep +mtlbuild-type:Customsetup-changed

Dependencies added: base, mtl

Files

• Control/Monad/Logic.hs +197/−0
• Control/Monad/Logic/Class.hs +157/−0
• LICENSE +12/−0
• Setup.lhs +4/−0
• logict.cabal +24/−0

@@ -0,0 +1,197 @@+{-# LANGUAGE UndecidableInstances #-}++-------------------------------------------------------------------------+-- |+-- Module      : Control.Monad.Logic+-- 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 (+    module Control.Monad.Logic.Class,+    -- * The Logic monad+    Logic(),+    runLogic,+    observe,+    observeMany,+    observeAll,+    -- * The LogicT monad transformer+    LogicT(),+    runLogicT,+    observeT,+    observeManyT,+    observeAllT,+    module Control.Monad,+    module Control.Monad.Trans+  ) where++import Control.Applicative++import Control.Monad+import Control.Monad.Identity+import Control.Monad.Trans++import Control.Monad.Reader.Class+import Control.Monad.State.Class++import qualified Data.Foldable as F+import qualified Data.Traversable as T++import Control.Monad.Logic.Class++-- An Applicative instance for Identity, as MTL lacks one, currently+instance Applicative Identity where+    pure = Identity+    (Identity f) <*> (Identity a) = Identity (f a)++type SK r a = a -> r -> r+type FK a = a++-------------------------------------------------------------------------+-- | A monad transformer for performing backtracking computations+-- layered over another monad 'm'+newtype LogicT m a =+    LogicT { unLogicT :: forall ans. SK (m ans) a -> FK (m ans) -> m ans }++-------------------------------------------------------------------------+-- | Extracts the first result from a LogicT computation,+-- failing otherwise.+observeT :: Monad m => LogicT m a -> m a+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 up to a given number of results from a LogicT computation.+observeManyT :: Monad m => Int -> LogicT m a -> m [a]+observeManyT n m+    | n <= 0 = return []+    | 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'++-------------------------------------------------------------------------+-- | Runs a LogicT computation with the specified initial success and+-- failure continuations.+runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r+runLogicT = unLogicT++-------------------------------------------------------------------------+-- | The basic Logic monad, for performing backtracking computations+-- returning values of type 'a'+newtype Logic a = Logic { unLogic :: LogicT Identity a }+--        deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadLogic)++-------------------------------------------------------------------------+-- | Extracts the first result from a Logic computation.+observe :: Logic a -> a+observe = runIdentity . observeT . unLogic++-------------------------------------------------------------------------+-- | Extracts all results from a Logic computation.+observeAll :: Logic a -> [a]+observeAll = runIdentity . observeAllT . unLogic++-------------------------------------------------------------------------+-- | Extracts up to a given number of results from a Logic computation.+observeMany :: Int -> Logic a -> [a]+observeMany i = runIdentity . observeManyT i . unLogic++-------------------------------------------------------------------------+-- | Runs a Logic computation with the specified initial success and+-- failure continuations.+runLogic :: Logic a -> (a -> r -> r) -> r -> r+runLogic l s f = runIdentity $ unLogicT (unLogic l) si fi+ where+ si = fmap . s+ fi = Identity f++instance (Functor f) => Functor (LogicT f) where+    fmap f lt = LogicT $ \sk fk -> unLogicT lt (sk . f) fk++instance (Applicative f) => 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++instance (Applicative f) => Alternative (LogicT f) where+    empty = LogicT $ \_ fk -> fk+    f1 <|> f2 = LogicT $ \sk fk -> unLogicT f1 sk (unLogicT f2 sk fk)++instance (Monad m) => Monad (LogicT m) where+    return a = LogicT $ \sk fk -> sk a fk+    m >>= f = LogicT $ \sk fk -> unLogicT m (\a fk' -> unLogicT (f a) sk fk') fk+    fail _ = LogicT $ \_ fk -> fk++instance (Monad m) => MonadPlus (LogicT m) where+    mzero = LogicT $ \_ fk -> fk+    m1 `mplus` m2 = LogicT $ \sk fk -> unLogicT m1 sk (unLogicT m2 sk fk)++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+    msplit m = lift $ unLogicT m ssk (return Nothing)+     where+     ssk a fk = return $ Just (a, (lift fk >>= reflect))++instance F.Foldable Logic where+    foldr f z l = runLogic l f z++instance T.Traversable Logic where+    traverse g l = runLogic l (\a ft -> cons <$> g a <*> ft) (pure mzero)+     where cons a l = return a `mplus` l++-- haddock doesn't like generalized newtype deriving, so I'm writing+-- instances by hand+instance Functor Logic where+    fmap f = Logic . fmap f . unLogic++instance Applicative Logic where+    pure = Logic . pure+    f <*> a = Logic $ unLogic f <*> unLogic a++instance Alternative Logic where+    empty = Logic empty+    a1 <|> a2 = Logic $ unLogic a1 <|> unLogic a2++instance Monad Logic where+    return = Logic . return+    m >>= f = Logic $ unLogic m >>= unLogic . f++instance MonadPlus Logic where+    mzero = Logic mzero+    m1 `mplus` m2 = Logic $ unLogic m1 `mplus` unLogic m2++instance MonadLogic Logic where+    msplit m = Logic . liftM (liftM (fmap Logic)) $ msplit (unLogic m)++-- Needs undecidable instances+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)++-- Needs undecidable instances+instance (MonadState s m) => MonadState s (LogicT m) where+    get = lift get+    put = lift . put+

@@ -0,0 +1,157 @@++-------------------------------------------------------------------------+-- |+-- 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 Control.Monad++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')++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')++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)++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)

@@ -0,0 +1,12 @@+This module is under this "3 clause" BSD license:++Copyright (c) 2007, Dan Doel+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.+    * The names of the contributors may not be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,4 @@+#!/usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain

@@ -0,0 +1,24 @@+Name:                   logict+Version:                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, Dan Doel+Author:                 Dan Doel+Maintainer:             dan.doel@gmail.com+Homepage:               http://code.haskell.org/~dolio/logict+Stability:              Experimental, based on paper+Tested-With:            GHC+Build-Depends:          base, mtl+Exposed-Modules:        Control.Monad.Logic,+                        Control.Monad.Logic.Class+Extensions:             MultiParamTypeClasses,+                        UndecidableInstances+GHC-Options:            -O2+