streamt (empty) → 0.5.0.0
raw patch · 8 files changed
+1082/−0 lines, 8 filesdep +asyncdep +basedep +criterionsetup-changed
Dependencies added: async, base, criterion, hspec, logict, mtl, streamt, tasty, tasty-hunit
Files
- LICENSE +33/−0
- README.md +20/−0
- Setup.hs +4/−0
- src/Control/Monad/Stream.hs +247/−0
- streamt.cabal +83/−0
- test/benchmarks.hs +40/−0
- test/logic.hs +537/−0
- test/microkanren.hs +118/−0
+ LICENSE view
@@ -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.+
+ README.md view
@@ -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+
+ Setup.hs view
@@ -0,0 +1,4 @@+import Distribution.Simple++main = defaultMain+
+ src/Control/Monad/Stream.hs view
@@ -0,0 +1,247 @@+-- |+-- Module : Control.Monad.Stream+-- Copyright : Oleg Kiselyov, Sebastian Fischer, David A Roberts+-- License : BSD3+-- +-- Maintainer : David A Roberts <d@vidr.cc>+-- 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:+-- <http://okmij.org/ftp/Computation/monads.html#fair-bt-stream>+-- +-- 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
+ streamt.cabal view
@@ -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 <d@vidr.cc>+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
+ test/benchmarks.hs view
@@ -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
+ test/logic.hs view
@@ -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
+ test/microkanren.hs view
@@ -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"))]