-
Notifications
You must be signed in to change notification settings - Fork 53
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Binary nondeterminism #197
Changes from 37 commits
8edd680
eb45dda
91be10b
162d626
1900a53
f3c830f
83cbf16
c80d652
991e55c
34a9979
8359300
6bd09c1
5ec21db
ae79dad
a37b26e
b72a107
c53a119
20bdb4b
42bdf1b
cf3db93
5ae55a2
8d0cf59
acadd3b
6460e72
b8f9b15
99b748f
d2bbd2d
73a8ba3
725cec1
dd85cf0
a7db05e
5674d9b
0a08f49
e70be43
3eabaf1
06dbd73
069c9cf
1bb5299
d4e1967
56d00bf
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -41,6 +41,7 @@ instance Effect Cull where | |
-- | Cull nondeterminism in the argument, returning at most one result. | ||
-- | ||
-- prop> run (runNonDet (runCull (cull (pure a <|> pure b)))) === [a] | ||
-- prop> run (runNonDet (runCull (cull (empty <|> pure a)))) === [a] | ||
-- prop> run (runNonDet (runCull (cull (pure a <|> pure b) <|> pure c))) === [a, c] | ||
-- prop> run (runNonDet (runCull (cull (asum (map pure (repeat a)))))) === [a] | ||
cull :: (Carrier sig m, Member Cull sig) => m a -> m a | ||
|
@@ -51,18 +52,20 @@ cull m = send (Cull m pure) | |
-- | ||
-- prop> run (runNonDet (runCull (pure a <|> pure b))) === [a, b] | ||
runCull :: Alternative m => CullC m a -> m a | ||
runCull (CullC m) = runNonDetC (runReader False m) ((<|>) . pure) empty | ||
runCull (CullC m) = runNonDetC (runReader False m) (<|>) pure empty | ||
|
||
newtype CullC m a = CullC { runCullC :: ReaderC Bool (NonDetC m) a } | ||
deriving (Applicative, Functor, Monad, Fail.MonadFail, MonadFix, MonadIO) | ||
|
||
instance Alternative (CullC m) where | ||
empty = CullC empty | ||
{-# INLINE empty #-} | ||
l <|> r = CullC $ ReaderC $ \ cull -> NonDetC $ \ cons nil -> do | ||
runNonDetC (runReader cull (runCullC l)) | ||
(\ a as -> cons a (if cull then nil else as)) | ||
(runNonDetC (runReader cull (runCullC r)) cons nil) | ||
l <|> r = CullC $ ReaderC $ \ cull -> | ||
if cull then | ||
NonDetC $ \ fork leaf nil -> | ||
runNonDetC (runReader cull (runCullC l)) fork leaf (runNonDetC (runReader cull (runCullC r)) fork leaf nil) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. When we’re inside a |
||
else | ||
runReader cull (runCullC l) <|> runReader cull (runCullC r) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. When we aren’t inside a |
||
{-# INLINE (<|>) #-} | ||
|
||
instance MonadPlus (CullC m) | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -102,15 +102,15 @@ instance Monad (CutC m) where | |
{-# INLINE (>>=) #-} | ||
|
||
instance Fail.MonadFail m => Fail.MonadFail (CutC m) where | ||
fail s = CutC (\ _ _ _ -> Fail.fail s) | ||
fail s = lift (Fail.fail s) | ||
{-# INLINE fail #-} | ||
|
||
instance MonadFix m => MonadFix (CutC m) where | ||
mfix f = CutC (\ cons nil _ -> mfix (\ a -> runCutC (f (head a)) (fmap . (:)) (pure []) (pure [])) >>= foldr cons nil) | ||
{-# INLINE mfix #-} | ||
|
||
instance MonadIO m => MonadIO (CutC m) where | ||
liftIO io = CutC (\ cons nil _ -> liftIO io >>= flip cons nil) | ||
liftIO io = lift (liftIO io) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I attempted to apply the same approach to There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you walk me through what’s going on here? I’m not sure I follow the operative difference introduced by this change. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The semantics are unchanged, because: lift m = CutC (\ cons nil _ -> m >>= flip cons nil) thus, lift (liftIO io) = CutC (\ cons nil _ -> liftIO io >>= flip cons nil) which is exactly the definition we’ve replaced. |
||
{-# INLINE liftIO #-} | ||
|
||
instance MonadPlus (CutC m) | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
{-# LANGUAGE DeriveAnyClass, DeriveFunctor, DeriveGeneric, DerivingStrategies, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeOperators, UndecidableInstances #-} | ||
{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeOperators, UndecidableInstances #-} | ||
module Control.Effect.NonDet | ||
( -- * NonDet effect | ||
NonDet(..) | ||
|
@@ -12,81 +12,117 @@ module Control.Effect.NonDet | |
, run | ||
) where | ||
|
||
import Control.Applicative (Alternative(..)) | ||
import Control.Applicative (Alternative(..), liftA2) | ||
import Control.Effect.Carrier | ||
import Control.Monad (MonadPlus(..)) | ||
import Control.Monad (MonadPlus(..), join) | ||
import qualified Control.Monad.Fail as Fail | ||
import Control.Monad.Fix | ||
import Control.Monad.IO.Class | ||
import Control.Monad.Trans.Class | ||
import Data.Maybe (fromJust) | ||
import GHC.Generics (Generic1) | ||
|
||
data NonDet m k | ||
= Empty | ||
| Choose (Bool -> m k) | ||
deriving stock (Functor, Generic1) | ||
deriving anyclass (HFunctor, Effect) | ||
deriving (Functor, Generic1) | ||
|
||
instance HFunctor NonDet | ||
instance Effect NonDet | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I honestly don’t think we should use There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Up to you. I personally like it, but given that it’s a two-line difference I’m not worked up about it. |
||
|
||
|
||
-- | Run a 'NonDet' effect, collecting all branches’ results into an 'Alternative' functor. | ||
-- | ||
-- Using '[]' as the 'Alternative' functor will produce all results, while 'Maybe' will return only the first. However, unlike 'runNonDetOnce', this will still enumerate the entire search space before returning, meaning that it will diverge for infinite search spaces, even when using 'Maybe'. | ||
-- Using @[]@ as the 'Alternative' functor will produce all results, while 'Maybe' will return only the first. However, unlike 'Control.Effect.Cull.runNonDetOnce', this will still enumerate the entire search space before returning, meaning that it will diverge for infinite search spaces, even when using 'Maybe'. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Haddock can’t link to |
||
-- | ||
-- prop> run (runNonDet (pure a)) === [a] | ||
-- prop> run (runNonDet (pure a)) === Just a | ||
runNonDet :: (Alternative f, Applicative m) => NonDetC m a -> m (f a) | ||
runNonDet (NonDetC m) = m (fmap . (<|>) . pure) (pure empty) | ||
runNonDet (NonDetC m) = m (liftA2 (<|>)) (pure . pure) (pure empty) | ||
|
||
-- | A carrier for 'NonDet' effects based on Ralf Hinze’s design described in [Deriving Backtracking Monad Transformers](https://www.cs.ox.ac.uk/ralf.hinze/publications/#P12). | ||
newtype NonDetC m a = NonDetC | ||
{ -- | A higher-order function receiving two parameters: a function to combine each solution with the rest of the solutions, and an action to run when no results are produced. | ||
runNonDetC :: forall b . (a -> m b -> m b) -> m b -> m b | ||
{ -- | A higher-order function receiving three continuations, respectively implementing '<|>', 'pure', and 'empty'. | ||
runNonDetC :: forall b . (m b -> m b -> m b) -> (a -> m b) -> m b -> m b | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is so much cleaner ✨ |
||
} | ||
deriving stock (Functor) | ||
deriving (Functor) | ||
|
||
-- $ | ||
-- prop> run (runNonDet (pure a *> pure b)) === Just b | ||
-- prop> run (runNonDet (pure a <* pure b)) === Just a | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. These sorts of tests of lawfulness strike me as something we could use more of. |
||
instance Applicative (NonDetC m) where | ||
pure a = NonDetC (\ cons -> cons a) | ||
pure a = NonDetC (\ _ leaf _ -> leaf a) | ||
{-# INLINE pure #-} | ||
NonDetC f <*> NonDetC a = NonDetC $ \ cons -> | ||
f (\ f' -> a (cons . f')) | ||
NonDetC f <*> NonDetC a = NonDetC $ \ fork leaf nil -> | ||
f fork (\ f' -> a fork (leaf . f') nil) nil | ||
{-# INLINE (<*>) #-} | ||
|
||
-- $ | ||
-- prop> run (runNonDet (pure a <|> (pure b <|> pure c))) === Fork (Leaf a) (Fork (Leaf b) (Leaf c)) | ||
-- prop> run (runNonDet ((pure a <|> pure b) <|> pure c)) === Fork (Fork (Leaf a) (Leaf b)) (Leaf c) | ||
instance Alternative (NonDetC m) where | ||
empty = NonDetC (\ _ nil -> nil) | ||
empty = NonDetC (\ _ _ nil -> nil) | ||
{-# INLINE empty #-} | ||
NonDetC l <|> NonDetC r = NonDetC $ \ cons -> l cons . r cons | ||
NonDetC l <|> NonDetC r = NonDetC $ \ fork leaf nil -> fork (l fork leaf nil) (r fork leaf nil) | ||
{-# INLINE (<|>) #-} | ||
|
||
instance Monad (NonDetC m) where | ||
NonDetC a >>= f = NonDetC $ \ cons -> | ||
a (\ a' -> runNonDetC (f a') cons) | ||
NonDetC a >>= f = NonDetC $ \ fork leaf nil -> | ||
a fork (\ a' -> runNonDetC (f a') fork leaf nil) nil | ||
{-# INLINE (>>=) #-} | ||
|
||
instance Fail.MonadFail m => Fail.MonadFail (NonDetC m) where | ||
fail s = NonDetC (\ _ _ -> Fail.fail s) | ||
fail s = lift (Fail.fail s) | ||
{-# INLINE fail #-} | ||
|
||
instance MonadFix m => MonadFix (NonDetC m) where | ||
mfix f = NonDetC (\ cons nil -> mfix (\ a -> runNonDetC (f (head a)) (fmap . (:)) (pure [])) >>= foldr cons nil) | ||
mfix f = NonDetC $ \ fork leaf nil -> | ||
mfix (\ a -> runNonDetC (f (fromJust (fold (<|>) Just Nothing a))) | ||
(liftA2 Fork) | ||
(pure . Leaf) | ||
(pure Nil)) | ||
>>= fold fork leaf nil | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Note that this implementation has the same behaviour as the previous one, and as such is subject to #209. I do not intend to fix that behaviour in this PR. |
||
{-# INLINE mfix #-} | ||
|
||
instance MonadIO m => MonadIO (NonDetC m) where | ||
liftIO io = NonDetC (\ cons nil -> liftIO io >>= flip cons nil) | ||
liftIO io = lift (liftIO io) | ||
{-# INLINE liftIO #-} | ||
|
||
instance MonadPlus (NonDetC m) | ||
|
||
instance MonadTrans NonDetC where | ||
lift m = NonDetC (\ cons nil -> m >>= flip cons nil) | ||
lift m = NonDetC (\ _ leaf _ -> m >>= leaf) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We no longer invoke the |
||
{-# INLINE lift #-} | ||
|
||
instance (Carrier sig m, Effect sig) => Carrier (NonDet :+: sig) (NonDetC m) where | ||
eff (L Empty) = empty | ||
eff (L (Choose k)) = k True <|> k False | ||
eff (R other) = NonDetC $ \ cons nil -> eff (handle [()] (fmap concat . traverse runNonDet) other) >>= foldr cons nil | ||
eff (R other) = NonDetC $ \ fork leaf nil -> eff (handle (Leaf ()) (fmap join . traverse runNonDet) other) >>= fold fork leaf nil | ||
{-# INLINE eff #-} | ||
|
||
|
||
data BinaryTree a = Nil | Leaf a | Fork (BinaryTree a) (BinaryTree a) | ||
deriving (Eq, Foldable, Functor, Ord, Show, Traversable) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I’ve opted not to export this for the time being, but I feel a bit weird about that. I don’t know that I really want to add a There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don’t object to keeping it hidden, personally. The more details we hide, the more we can iterate on the internals without breaking public API. We’re already entailing a good bit of churn these days, after all! There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. That is an excellent point. |
||
|
||
instance Applicative BinaryTree where | ||
pure = Leaf | ||
robrix marked this conversation as resolved.
Show resolved
Hide resolved
|
||
f <*> a = fold Fork (<$> a) Nil f | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This and the definition of |
||
|
||
instance Alternative BinaryTree where | ||
empty = Nil | ||
(<|>) = Fork | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We need the |
||
|
||
instance Monad BinaryTree where | ||
a >>= f = fold Fork f Nil a | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
|
||
|
||
fold :: (b -> b -> b) -> (a -> b) -> b -> BinaryTree a -> b | ||
fold fork leaf nil = go where | ||
go Nil = nil | ||
go (Leaf a) = leaf a | ||
go (Fork a b) = fork (go a) (go b) | ||
|
||
|
||
-- $setup | ||
-- >>> :seti -XFlexibleContexts | ||
-- >>> import Test.QuickCheck | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like that this got simpler.