diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,33 @@ +Copyright (c) 2010-2012, Sebastian Fischer +Copyright (c) 2021, David A Roberts + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. 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. + + 3. Neither the name of the author nor the names of his contributors + may 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 AUTHORS 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. + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,20 @@ +# Simple, Fair and Terminating Backtracking Monad Transformer + +This Haskell library provides an implementation of the MonadPlus type +class that enumerates results of a non-deterministic computation by +interleaving subcomputations in a way that has usually much better +memory performance than other strategies with the same termination +properties. + +It also terminates in many cases where the fair conjunction and +interleaving operators provided by LogicT fail to do so, allowing it +to safely provide fairness by default. + +More information is available on the [author's website][FBackTrackT]. + +This package aims to be a drop-in replacement for the unmaintained +`stream-monad` package, in addition to providing much of the same +functionality as the `logict` package. + +[FBackTrackT]: http://okmij.org/ftp/Computation/monads.html#fair-bt-stream + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,4 @@ +import Distribution.Simple + +main = defaultMain + diff --git a/src/Control/Monad/Stream.hs b/src/Control/Monad/Stream.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Stream.hs @@ -0,0 +1,247 @@ +-- | +-- Module : Control.Monad.Stream +-- Copyright : Oleg Kiselyov, Sebastian Fischer, David A Roberts +-- License : BSD3 +-- +-- Maintainer : David A Roberts +-- Stability : experimental +-- Portability : portable +-- +-- This Haskell library provides an implementation of the MonadPlus +-- type class that enumerates results of a non-deterministic +-- computation by interleaving subcomputations in a way that has +-- usually much better memory performance than other strategies with +-- the same termination properties. +-- +-- By using supensions in strategic positions, the user can ensure +-- that the search does not diverge if there are remaining +-- non-deterministic results. +-- +-- More information is available on the author's website: +-- +-- +-- Warning: @Stream@ is only a monad when the results of @observeAll@ +-- are interpreted as a multiset, i.e., a valid transformation +-- according to the monad laws may change the order of the results. +-- +{-# LANGUAGE CPP, FlexibleInstances, LambdaCase, + MultiParamTypeClasses, UndecidableInstances #-} + +module Control.Monad.Stream + ( StreamT + , Stream + , suspended + , runStream + , observe + , observeT + , observeAll + , observeAllT + , observeMany + , observeManyT + , module Control.Monad.Logic.Class + ) where + +import Control.Applicative (Alternative(..), (<**>)) +import Control.Monad (MonadPlus(..), liftM) +import qualified Control.Monad.Fail as Fail +import Control.Monad.Identity (Identity(..)) +import Control.Monad.Logic.Class +import Control.Monad.Reader.Class (MonadReader(..)) +import Control.Monad.State.Class (MonadState(..)) +import Control.Monad.Trans (MonadIO(..), MonadTrans(..)) +import qualified Data.Foldable as F +#if !MIN_VERSION_base(4,8,0) +import Data.Monoid (Monoid(..)) +#endif +#if MIN_VERSION_base(4,9,0) +import Data.Semigroup (Semigroup(..)) +#endif + +data StreamF s a + = Nil + | Single a + | Cons a s + | Susp s + +-- | +-- Results of non-deterministic computations of type @StreamT m a@ can be +-- enumerated efficiently. +-- +newtype StreamT m a = + StreamT + { unStreamT :: m (StreamF (StreamT m a) a) + } + +type Stream = StreamT Identity + +-- | +-- Suspensions can be used to ensure fairness. +-- +suspended :: Monad m => StreamT m a -> StreamT m a +suspended = StreamT . return . Susp + +cons :: Monad m => a -> StreamT m a -> StreamT m a +cons a = StreamT . return . Cons a + +bind :: + Monad m + => StreamT m a + -> (StreamF (StreamT m a) a -> StreamT m b) + -> StreamT m b +bind m f = StreamT $ unStreamT m >>= unStreamT . f + +-- | +-- The function @runStream@ enumerates the results of a +-- non-deterministic computation. +-- +runStream :: Stream a -> [a] +runStream = observeAll + +{-# DEPRECATED +runStream "use observeAll" + #-} + +instance Monad m => Monad (StreamT m) where + return = pure + m >>= f = + m `bind` \case + Nil -> empty + Single x -> f x + Cons x xs -> f x <|> suspended (xs >>= f) + Susp xs -> suspended (xs >>= f) +#if !MIN_VERSION_base(4,13,0) + fail = Fail.fail +#endif +instance Monad m => Fail.MonadFail (StreamT m) where + fail _ = empty + +instance Monad m => Alternative (StreamT m) where + empty = StreamT $ return Nil + m <|> ys = + m `bind` \case + Nil -> suspended ys -- suspending + Single x -> cons x ys + Cons x xs -> cons x (ys <|> xs) -- interleaving + Susp xs -> + ys `bind` \case + Nil -> suspended xs + Single y -> cons y xs + Cons y ys' -> cons y (xs <|> ys') + Susp ys' -> suspended (xs <|> ys') + +instance Monad m => MonadPlus (StreamT m) where + mzero = empty + mplus = (<|>) +#if MIN_VERSION_base(4,9,0) +instance Monad m => Semigroup (StreamT m a) where + (<>) = mplus + sconcat = foldr1 mplus +#endif +instance Monad m => Monoid (StreamT m a) where + mempty = empty + mappend = (<|>) + mconcat = F.asum + +instance Monad m => Functor (StreamT m) where + fmap f m = + m `bind` \case + Nil -> empty + Single x -> return (f x) + Cons x xs -> cons (f x) (fmap f xs) + Susp xs -> suspended (fmap f xs) + +instance Monad m => Applicative (StreamT m) where + pure = StreamT . return . Single + m <*> xs = + m `bind` \case + Nil -> empty + Single f -> fmap f xs + Cons f fs -> fmap f xs <|> (xs <**> fs) + Susp fs -> suspended (xs <**> fs) + +instance Monad m => MonadLogic (StreamT m) where + (>>-) = (>>=) + interleave = mplus + msplit m = + m `bind` \case + Nil -> return Nothing + Single x -> return $ Just (x, empty) + Cons x xs -> return $ Just (x, suspended xs) + Susp xs -> suspended $ msplit xs + +instance MonadTrans StreamT where + lift = StreamT . liftM Single + +instance MonadIO m => MonadIO (StreamT m) where + liftIO = lift . liftIO + +instance MonadReader r m => MonadReader r (StreamT m) where + ask = lift ask + local f = StreamT . local f . unStreamT + +instance MonadState s m => MonadState s (StreamT m) where + get = lift get + put = lift . put + +instance (Monad m, Foldable m) => Foldable (StreamT m) where + foldMap f = foldMap g . unStreamT + where + g Nil = mempty + g (Single x) = f x + g (Cons x xs) = f x `mappend` foldMap f xs + g (Susp xs) = foldMap f xs + +instance (Monad m, Traversable m) => Traversable (StreamT m) where + traverse f = fmap StreamT . traverse g . unStreamT + where + g Nil = pure Nil + g (Single x) = Single <$> f x + g (Cons x xs) = Cons <$> f x <*> traverse f xs + g (Susp xs) = Susp <$> traverse f xs + +observeAllT :: Monad m => StreamT m a -> m [a] +observeAllT m = + unStreamT m >>= \case + Nil -> return [] + Single a -> return [a] + Cons a r -> do + t <- observeAllT r + return (a : t) + Susp r -> observeAllT r + +observeAll :: Stream a -> [a] +observeAll = runIdentity . observeAllT + +observeManyT :: Monad m => Int -> StreamT m a -> m [a] +observeManyT 0 _ = return [] +observeManyT n m = + unStreamT m >>= \case + Nil -> return [] + Single a -> return [a] + Cons a r -> do + t <- observeManyT (n - 1) r + return (a : t) + Susp r -> observeManyT n r + +observeMany :: Int -> Stream a -> [a] +observeMany n = runIdentity . observeManyT n + +#if !MIN_VERSION_base(4,13,0) +observeT :: Monad m => StreamT m a -> m a +#else +observeT :: MonadFail m => StreamT m a -> m a +#endif +observeT m = + unStreamT m >>= \case + Nil -> fail "No answer." + Single a -> return a + Cons a _ -> return a + Susp r -> observeT r + +observe :: Stream a -> a +observe m = + case runIdentity (unStreamT m) of + Nil -> error "No answer." + Single a -> a + Cons a _ -> a + Susp r -> observe r diff --git a/streamt.cabal b/streamt.cabal new file mode 100644 --- /dev/null +++ b/streamt.cabal @@ -0,0 +1,83 @@ +name: streamt +version: 0.5.0.0 +cabal-version: >=1.10 +synopsis: Simple, Fair and Terminating Backtracking Monad Transformer +description: + This Haskell library provides an implementation of the + MonadPlus type class that enumerates results of a + non-deterministic computation by interleaving + subcomputations in a way that has usually much better + memory performance than other strategies with the same + termination properties. + +category: Control, Monads +license: BSD3 +license-file: LICENSE +author: Oleg Kiselyov, Sebastian Fischer, David A Roberts +maintainer: David A Roberts +bug-reports: http://github.com/davidar/streamt/issues +homepage: http://github.com/davidar/streamt +build-type: Simple +stability: experimental +tested-with: + GHC ==8.0.2 + || ==8.2.2 + || ==8.4.4 + || ==8.6.5 + || ==8.8.4 + || ==8.10.4 + || ==9.0.1 + +extra-source-files: README.md + +library + build-depends: + base >=4.3 && <5 + , logict >=0.7 && <0.8 + , mtl >=2.0 && <2.3 + + hs-source-dirs: src + exposed-modules: Control.Monad.Stream + ghc-options: -Wall + default-language: Haskell2010 + +test-suite streamt-benchmarks + main-is: benchmarks.hs + build-depends: + base >=3 && <5 + , criterion >=0.5 + , streamt + + hs-source-dirs: test + type: exitcode-stdio-1.0 + default-language: Haskell2010 + +test-suite streamt-microkanren + main-is: microkanren.hs + build-depends: + base + , hspec + , mtl + , streamt + + hs-source-dirs: test + type: exitcode-stdio-1.0 + default-language: Haskell2010 + +test-suite streamt-logic + main-is: logic.hs + build-depends: + async >=2.0 + , base + , mtl + , streamt + , tasty + , tasty-hunit + + hs-source-dirs: test + type: exitcode-stdio-1.0 + default-language: Haskell2010 + +source-repository head + type: git + location: git://github.com/davidar/streamt.git diff --git a/test/benchmarks.hs b/test/benchmarks.hs new file mode 100644 --- /dev/null +++ b/test/benchmarks.hs @@ -0,0 +1,40 @@ +import Criterion.Main (defaultMain, bench, nf) +import Control.Monad (guard, MonadPlus(..)) +import Control.Monad.Stream (Stream) +import Data.Foldable (Foldable(toList)) + +main :: IO () +main = defaultMain + [ bench "permsort" $ nf (toList . permSort) ([1..4]++[8,7..5]), + bench "8 queens" $ nf (toList . nQueens) 8 ] + +permSort :: [Int] -> Stream [Int] +permSort xs = do ys <- permute xs + guard (ascending ys) + return ys + +permute :: [a] -> Stream [a] +permute [] = return [] +permute xs = do (y,ys) <- select xs + zs <- permute ys + return (y:zs) + +select :: [a] -> Stream (a,[a]) +select [] = mzero +select (x:xs) = return (x,xs) + `mplus` do (y,ys) <- select xs + return (y,x:ys) + +ascending :: [Int] -> Bool +ascending [] = True +ascending [_] = True +ascending (x:y:zs) = x <= y && ascending (y:zs) + +nQueens :: Int -> Stream [Int] +nQueens n = do qs <- permute [1..n] + guard (safe qs) + return qs + +safe :: [Int] -> Bool +safe qs = and [ j-i /= abs (qj-qi) | (i,qi) <- iqs, (j,qj) <- iqs, i < j ] + where iqs = zip [1..] qs diff --git a/test/logic.hs b/test/logic.hs new file mode 100644 --- /dev/null +++ b/test/logic.hs @@ -0,0 +1,537 @@ +-- based on the logict test-suite +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} + +module Main where + +import Test.Tasty +import Test.Tasty.HUnit + +import Control.Arrow ( left ) +import Control.Concurrent ( threadDelay ) +import Control.Concurrent.Async ( race ) +import Control.Exception +import Control.Monad.Identity +import Control.Monad.Stream +import Control.Monad.Reader +import qualified Control.Monad.State.Lazy as SL +import qualified Control.Monad.State.Strict as SS +import Data.Maybe + +#if MIN_VERSION_base(4,9,0) +#if MIN_VERSION_base(4,11,0) +#else +import Data.Semigroup (Semigroup (..)) +#endif +#else +import Data.Monoid +#endif + + +monadReader1 :: Assertion +monadReader1 = assertEqual "should be equal" [5 :: Int] $ + runReader (observeAllT (local (+ 5) ask)) 0 + +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 => StreamT m Integer + +#if MIN_VERSION_base(4,8,0) +nats = pure 0 `mplus` ((1 +) <$> nats) +#else +nats = return 0 `mplus` liftM (1 +) nats +#endif + +odds = return 1 `mplus` liftM (2+) odds + +oddsOrTwoUnfair = odds `mplus` return 2 +oddsOrTwoFair = odds `interleave` return 2 + +oddsOrTwo = do x <- oddsOrTwoFair + if even x then once (return x) else mzero + +odds5down = return 5 `mplus` mempty `mplus` mempty `mplus` return 3 `mplus` return 1 + +pythagoreanTriples :: MonadPlus m => m (Int,Int,Int) +pythagoreanTriples = do + let number = (return 0) `mplus` (number >>= return . succ) + i <- number + guard $ i > 0 + j <- number + guard $ j > 0 + k <- number + guard $ k > 0 + guard $ i*i + j*j == k*k + return (i,j,k) + +pythagoreanTriplesLeftRecursion :: Monad m => StreamT m (Int,Int,Int) +pythagoreanTriplesLeftRecursion = do + let number = (suspended number >>= return . succ) `mplus` return 0 + i <- number + j <- number + k <- number + guard $ i*i + j*j == k*k + return (i,j,k) + +-- a serious test of left recursion (due to Will Byrd) +flaz :: Int -> Stream Int +flaz x = suspended (flaz x) `mplus` (suspended (flaz x) `mplus` if x == 5 then return x else mzero) + + +main :: IO () +main = defaultMain $ +#if __GLASGOW_HASKELL__ >= 702 + localOption (mkTimeout 3000000) $ -- 3 second deadman timeout +#endif + testGroup "All" + [ testGroup "Monad Reader + env" + [ testCase "Monad Reader 1" monadReader1 + , testCase "Monad Reader 2" monadReader2 + , testCase "Monad Reader 3" monadReader3 + ] + + , testGroup "Various monads" + [ + -- nats will generate an infinite number of results; demonstrate + -- various ways of observing them via Stream/StreamT + 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 StreamT 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 compatibility tests" + [ + testCase "observe multi" $ 5 @=? observe odds5down + , testCase "observe none" $ (Left "No answer." @=?) =<< safely (observe mzero) + + , testCase "observeAll multi" $ [5,1,3] @=? observeAll odds5down + , testCase "observeAll none" $ ([] :: [Integer]) @=? observeAll mzero + + , testCase "observeMany multi" $ [5,1] @=? observeMany 2 odds5down + , testCase "observeMany none" $ ([] :: [Integer]) @=? observeMany 2 mzero + ] + + -------------------------------------------------- + + , testGroup "Control.Monad.Stream tests" + [ + testCase "Pythagorean triples" $ [(3,4,5),(4,3,5),(6,8,10),(8,6,10),(5,12,13),(12,5,13),(9,12,15)] @=? + observeMany 7 pythagoreanTriples + + , testCase "Pythagorean triples (left recursion)" $ [(3,4,5),(4,3,5),(6,8,10),(8,6,10)] @=? + filter (\(i,j,k) -> i /= 0 && j /= 0 && k /= 0) + (observeMany 27 pythagoreanTriplesLeftRecursion) + + , testCase "flaz (left recursion)" $ replicate 15 5 @=? + observeMany 15 (flaz 5) + ] + + -------------------------------------------------- + + , testGroup "Control.Monad.Logic.Class tests" + [ + testGroup "msplit laws" + [ + testGroup "msplit mzero == return Nothing" + [ + testCase "msplit mzero :: []" $ + msplit mzero @=? return (Nothing :: Maybe (String, [String])) + + , testCase "msplit mzero :: ReaderT" $ + let z :: ReaderT Int [] String + z = mzero + in assertBool "ReaderT" $ null $ catMaybes $ runReaderT (msplit z) 0 + + , testCase "msplit mzero :: StreamT" $ + let z :: StreamT [] String + z = mzero + in assertBool "StreamT" $ null $ catMaybes $ concat $ observeAllT (msplit z) + , testCase "msplit mzero :: strict StateT" $ + let z :: SS.StateT Int [] String + z = mzero + in assertBool "strict StateT" $ null $ catMaybes $ SS.evalStateT (msplit z) 0 + , testCase "msplit mzero :: lazy StateT" $ + let z :: SL.StateT Int [] String + z = mzero + in assertBool "lazy StateT" $ null $ catMaybes $ SL.evalStateT (msplit z) 0 + ] + + , testGroup "msplit (return a `mplus` m) == return (Just a, m)" $ + let sample = [1::Integer,2,3] in + [ + testCase "msplit []" $ do + let op = sample + extract = fmap (fmap fst) + extract (msplit op) @?= [Just 1] + extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= [Just 2] + + , testCase "msplit ReaderT" $ do + let op = ask + extract = fmap fst . catMaybes . flip runReaderT sample + extract (msplit op) @?= [sample] + extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= [] + + , testCase "msplit StreamT" $ do + let op :: StreamT [] Integer + op = foldr (mplus . return) mzero sample + extract = fmap fst . catMaybes . concat . observeAllT + extract (msplit op) @?= [1] + extract (msplit op >>= (\(Just (_,nxt)) -> msplit nxt)) @?= [2] + + , testCase "msplit strict StateT" $ do + let op :: SS.StateT Integer [] Integer + op = (SS.modify (+1) >> SS.get `mplus` op) + extract = fmap fst . catMaybes . flip SS.evalStateT 0 + extract (msplit op) @?= [1] + extract (msplit op >>= \(Just (_,nxt)) -> msplit nxt) @?= [2] + + , testCase "msplit lazy StateT" $ do + let op :: SL.StateT Integer [] Integer + op = (SL.modify (+1) >> SL.get `mplus` op) + extract = fmap fst . catMaybes . flip SL.evalStateT 0 + extract (msplit op) @?= [1] + extract (msplit op >>= \(Just (_,nxt)) -> msplit nxt) @?= [2] + ] + ] + + , testGroup "fair disjunction" + [ + -- base case + testCase "some odds" $ [1,3,5,7] @=? observeMany 4 odds + + -- identical to fair disjunction + , testCase "unfair disjunction" $ [1,2,3,5] @=? observeMany 4 oddsOrTwoUnfair + + -- with fairness, the results are interleaved + + , testCase "fair disjunction :: StreamT" $ [1,2,3,5] @=? observeMany 4 oddsOrTwoFair + + -- without fairness nothing would be produced, but with + -- fairness, a production is obtained + + , testCase "fair production" $ [2] @=? observeT oddsOrTwo + + -- however, asking for additional productions will not + -- terminate (there are none, since the first clause generates + -- an infinity of mzero "failures") + + , testCase "NONTERMINATION even when fair" $ + (Left () @=?) =<< (nonTerminating $ observeManyT 2 oddsOrTwo) + + -- Validate fair disjunction works for other + -- Control.Monad.Logic.Class instances + + , testCase "fair disjunction :: []" $ [1,2,3,5] @=? + (take 4 $ let oddsL = [ 1::Integer ] `mplus` [ o | o <- [3..], odd o ] + oddsOrTwoLFair = oddsL `interleave` [2] + in oddsOrTwoLFair) + + , testCase "fair disjunction :: ReaderT" $ [1,2,3,5] @=? + (take 4 $ runReaderT (let oddsR = return 1 `mplus` liftM (2+) oddsR + in oddsR `interleave` return (2 :: Integer)) "go") + + , testCase "fair disjunction :: strict StateT" $ [1,2,3,5] @=? + (take 4 $ SS.evalStateT (let oddsS = return 1 `mplus` liftM (2+) oddsS + in oddsS `interleave` return (2 :: Integer)) "go") + + , testCase "fair disjunction :: lazy StateT" $ [1,2,3,5] @=? + (take 4 $ SL.evalStateT (let oddsS = return 1 `mplus` liftM (2+) oddsS + in oddsS `interleave` return (2 :: Integer)) "go") + ] + + , testGroup "fair conjunction" $ + [ + -- Using the fair conjunction operator (>>-) the test produces values + + testCase "fair conjunction :: StreamT" $ [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 produces values because interleaving suspended + -- Streams does *not* require production of values from + -- branches to switch between them (the first + -- (oddsPlus 0 ...) never produces any values). + + , testCase "fair conjunction PRODUCTIVE" $ [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) + ) + + -- This shows that the second >>- is effectively >>= since + -- there's no choice point for it, and values can still be + -- produced. + + , testCase "fair conjunction also PRODUCTIVE" $ [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) + ) + + -- identical to fair conjunction + + , testCase "unfair conjunction is PRODUCTIVE" $ [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 + ) + + , testCase "fair conjunction :: []" $ [2,4,6,8] @=? + (take 4 $ let oddsL = [ 1 :: Integer ] `mplus` [ o | o <- [3..], odd o ] + oddsPlus n = [ a + n | a <- oddsL ] + in do x <- [0] `mplus` [1] >>- oddsPlus + if even x then return x else mzero + ) + + , testCase "fair conjunction :: ReaderT" $ [2,4,6,8] @=? + (take 4 $ runReaderT (let oddsR = return (1 :: Integer) `mplus` liftM (2+) oddsR + oddsPlus n = oddsR >>= \a -> return (a + n) + in do x <- (return 0 `mplus` return 1) >>- oddsPlus + if even x then return x else mzero + ) "env") + + , testCase "fair conjunction :: strict StateT" $ [2,4,6,8] @=? + (take 4 $ SS.evalStateT (let oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS + oddsPlus n = oddsS >>= \a -> return (a + n) + in do x <- (return 0 `mplus` return 1) >>- oddsPlus + if even x then return x else mzero + ) "state") + + , testCase "fair conjunction :: lazy StateT" $ [2,4,6,8] @=? + (take 4 $ SL.evalStateT (let oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS + oddsPlus n = oddsS >>= \a -> return (a + n) + in do x <- (return 0 `mplus` return 1) >>- oddsPlus + if even x then return x else mzero + ) "env") + ] + + , testGroup "ifte logical conditional (soft-cut)" + [ + -- Initial example returns all odds which are divisible by + -- another number. Nothing special is needed to implement this. + + let iota n = msum (map return [1..n]) + oc = do n <- odds + guard (n > 1) + d <- iota (n - 1) + guard (d > 1 && n `mod` d == 0) + return n + in testCase "divisible odds" $ [9,15,15,21,21,25,27,27,33,33] @=? + observeMany 10 oc + + -- To get the inverse: all odds which are *not* divisible by + -- another number, the guard test cannot simply be reversed: + -- there are many produced values that are not divisors, but + -- some that are: + + , let iota n = msum (map return [1..n]) + oc = do n <- odds + guard (n > 1) + d <- iota (n - 1) + guard (d > 1 && n `mod` d /= 0) + return n + in testCase "indivisible odds, wrong" $ + [3,5,5,7,5,7,7,9,7,7] @=? + 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 :: StreamT" $ [3,5,7,11,13,17,19,23,29,31] @=? + observeMany 10 oc + + , let iota n = [1..n] + oddsL = [ 1 :: Integer ] `mplus` [ o | o <- [3..], odd o ] + oc = [ n + | n <- oddsL + , (n > 1) + ] >>= \n -> ifte (do d <- iota (n - 1) + guard (d > 1 && n `mod` d == 0)) + (const mzero) + (return n) + in testCase "indivisible odds :: []" $ [3,5,7,11,13,17,19,23,29,31] @=? + take 10 oc + + , let iota n = msum (map return [1..n]) + oddsR = return (1 :: Integer) `mplus` liftM (2+) oddsR + oc = do n <- oddsR + guard (n > 1) + ifte (do d <- iota (n - 1) + guard (d > 1 && n `mod` d == 0)) + (const mzero) + (return n) + in testCase "indivisible odds :: ReaderT" $ [3,5,7,11,13,17,19,23,29,31] @=? + (take 10 $ runReaderT oc "env") + + , let iota n = msum (map return [1..n]) + oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS + oc = do n <- oddsS + guard (n > 1) + ifte (do d <- iota (n - 1) + guard (d > 1 && n `mod` d == 0)) + (const mzero) + (return n) + in testCase "indivisible odds :: strict StateT" $ [3,5,7,11,13,17,19,23,29,31] @=? + (take 10 $ SS.evalStateT oc "state") + + , let iota n = msum (map return [1..n]) + oddsS = return (1 :: Integer) `mplus` liftM (2+) oddsS + oc = do n <- oddsS + guard (n > 1) + ifte (do d <- iota (n - 1) + guard (d > 1 && n `mod` d == 0)) + (const mzero) + (return n) + in testCase "indivisible odds :: strict StateT" $ [3,5,7,11,13,17,19,23,29,31] @=? + (take 10 $ SL.evalStateT oc "state") + + ] + + , testGroup "once (pruning)" $ + -- the pruning primitive 'once' selects (non-deterministically) + -- a single candidate from many results and disables any further + -- backtracking on this choice. + + let bogosort l = do p <- permute l + if sorted p then return p else mzero + + sorted (e:e':r) = e <= e' && sorted (e':r) + sorted _ = True + + permute [] = return [] + permute (h:t) = do { t' <- permute t; insert h t' } + + insert e [] = return [e] + insert e l@(h:t) = return (e:l) `mplus` + do { t' <- insert e t; return (h : t') } + + inp = [5,0,3,4,0,1 :: Integer] + in + [ + -- without pruning, get two results because 0 appears twice + testCase "no pruning" $ [[0,0,1,3,4,5], [0,0,1,3,4,5]] @=? + observeAll (bogosort inp) + + -- with pruning, stops after the first result + , testCase "with pruning" $ [[0,0,1,3,4,5]] @=? + observeAll (once (bogosort inp)) + ] + ] + + , testGroup "lnot (inversion)" $ + let isEven n = if even n then return n else mzero in + [ + testCase "inversion :: StreamT" $ [1,3,5,7,9] @=? + observeMany 5 (do v <- foldr (mplus . return) mzero [(1::Integer)..] + lnot (isEven v) + return v) + + , testCase "inversion :: []" $ [1,3,5,7,9] @=? + (take 5 $ do v <- [(1::Integer)..] + lnot (isEven v) + return v) + + , testCase "inversion :: ReaderT" $ [1,3,5,7,9] @=? + (take 5 $ runReaderT (do v <- foldr (mplus . return) mzero [(1::Integer)..] + lnot (isEven v) + return v) "env") + + , testCase "inversion :: strict StateT" $ [1,3,5,7,9] @=? + (take 5 $ SS.evalStateT (do v <- foldr (mplus . return) mzero [(1::Integer)..] + lnot (isEven v) + return v) "state") + + , testCase "inversion :: lazy StateT" $ [1,3,5,7,9] @=? + (take 5 $ SL.evalStateT (do v <- foldr (mplus . return) mzero [(1::Integer)..] + lnot (isEven v) + return v) "state") + ] + ] + +safely :: IO Integer -> IO (Either String Integer) +safely o = fmap (left (head . lines . show)) (try o :: IO (Either SomeException Integer)) + +-- | This is used to test logic operations that don't typically +-- terminate by running a parallel race between the operation and a +-- timer. A result of @Left ()@ means that the timer won and the +-- operation did not terminate within that time period. + +nonTerminating :: IO a -> IO (Either () a) +nonTerminating op = race (threadDelay 100000) op -- returns Left () after 0.1s diff --git a/test/microkanren.hs b/test/microkanren.hs new file mode 100644 --- /dev/null +++ b/test/microkanren.hs @@ -0,0 +1,118 @@ +-- https://gist.github.com/msullivan/4223fd47991acbe045ec +import Control.Applicative (Alternative(..)) +import Control.Monad (MonadPlus(..)) +import qualified Control.Monad.Stream as Stream +import Control.Monad.Stream (Stream) +import Control.Monad.State (MonadState(..), StateT(..), execStateT, mapStateT) +import Test.Hspec (hspec, it, shouldBe) + +type Var = Integer +type Subst = [(Var, Term)] +type State = (Subst, Integer) +type Program = StateT State Stream + +data Term = Atom String | Pair Term Term | Var Var deriving (Eq, Show) + +-- Apply a substitution to the top level of a term +walk :: Term -> Subst -> Term +walk (Var v) s = case lookup v s of Nothing -> Var v + Just us -> walk us s +walk u s = u + +extS :: Var -> Term -> Subst -> Subst +extS x v s = (x, v) : s + +-- Try to unify two terms under a substitution; +-- return an extended subst if it succeeds +unify :: Term -> Term -> Subst -> Maybe Subst +unify u v s = un (walk u s) (walk v s) + where un (Var x1) (Var x2) | x1 == x2 = return s + un (Var x1) v = return $ extS x1 v s + un u (Var x2) = return $ extS x2 u s + un (Pair u1 u2) (Pair v1 v2) = + do s' <- unify u1 v1 s + unify u2 v2 s' + un (Atom a1) (Atom a2) | a1 == a2 = return s + un _ _ = mzero + +fresh :: Program Term +fresh = do + (s, c) <- get + put (s, c+1) + return (Var c) + +-- microKanren program formers +zzz :: Program a -> Program a +zzz = mapStateT Stream.suspended + +equiv :: Term -> Term -> Program () +equiv u v = do + (s, c) <- get + case unify u v s of + Nothing -> mzero + Just s' -> put (s', c) + +callFresh :: (Term -> Program a) -> Program a +callFresh = (fresh >>=) + +disj :: Program a -> Program a -> Program a +disj = (<|>) + +conj :: Program a -> Program b -> Program b +conj = (>>) + +-- Recovering miniKanren interface +reify :: [State] -> [Term] +reify = map reifyState + where + reifyState :: State -> Term + reifyState (s, _) = let v = walk' (Var 0) s in walk' v (reifyS v []) + + reifyS :: Term -> Subst -> Subst + reifyS v s = case walk v s of + Var v -> let n = reifyName (length s) in (v, n) : s + Pair u v -> reifyS v $ reifyS u s + _ -> s + + reifyName :: Int -> Term + reifyName n = Atom $ "_." ++ show n + + walk' :: Term -> Subst -> Term + walk' v s = case walk v s of + Pair u v -> Pair (walk' u s) (walk' v s) + v -> v + +callEmptyState :: Program () -> Stream State +callEmptyState g = execStateT g ([], 0) + +run :: Int -> (Term -> Program ()) -> [Term] +run n = reify . Stream.observeMany n . callEmptyState . callFresh + +run' :: (Term -> Program ()) -> [Term] +run' = reify . Stream.observeAll . callEmptyState . callFresh + +-- Tests +main :: IO () +main = hspec $ do + let ab = conj + (callFresh (\a -> equiv a (Atom "7"))) + (callFresh (\b -> disj (equiv b (Atom "5")) (equiv b (Atom "6")))) + five x = equiv x (Atom "5") + fives x = disj (equiv x (Atom "5")) (zzz $ fives x) + fivesRev x = disj (zzz $ fivesRev x) (equiv x (Atom "5")) + sixes x = disj (equiv x (Atom "6")) (zzz $ sixes x) + p56 x = disj (fives x) (sixes x) + p010 q = do + x <- fresh; y <- fresh + equiv q (Pair x (Pair y x)) <|> equiv q (Pair y (Pair x y)) + it "ab" $ Stream.observeAll (callEmptyState ab) `shouldBe` + [([(1,Atom "5"),(0,Atom "7")],2) + ,([(1,Atom "6"),(0,Atom "7")],2)] + it "five" $ run' five `shouldBe` [Atom "5"] + it "fives" $ run 10 fives `shouldBe` replicate 10 (Atom "5") + it "fivesRev" $ run 10 fivesRev `shouldBe` replicate 10 (Atom "5") + it "p56" $ run 10 p56 `shouldBe` concat (replicate 5 [Atom "5",Atom "6"]) + it "null" $ run' (const $ pure ()) `shouldBe` [Atom "_.0"] + it "p010" $ run 2 p010 `shouldBe` + [Pair (Atom "_.0") (Pair (Atom "_.1") (Atom "_.0")) + ,Pair (Atom "_.0") (Pair (Atom "_.1") (Atom "_.0"))]