-
Notifications
You must be signed in to change notification settings - Fork 73
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
Core rewrite for new family of easy higher-order interpreters #397
Conversation
-- | ||
-- @since TODO | ||
interpretNew :: forall e r a | ||
. (forall z x. e z x -> Sem (RunH z ': r) x) |
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've decided not to expose z ~ Sem rInitial
. The reason that's important for interpretH
and friends is because effectful state makes it difficult to combine or manipulate higher-order thunks in the Tactical
enviroment. But interpretNew
doesn't involve effectful state threading -- so you can simply convert thunks through runH
, and then combine them willy-nilly.
data Zip :: Effect where
Zip :: m a -> m b -> Zip m (a, b)
runZip :: Sem (Zip ': r) a -> Sem r a
runZip = interpretNew $ \case
Zip ma mb -> (,) <$> runH ma <*> runH mb
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.
would it be possible at all to switch the interpreter for higher order actions without Tactics
?
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.
It is, but it'd require exposing the fact that there's a MonadTransControl
involved, complicating the interface. It'd look something like this:
data RunH z t e r m a where
RunH :: z a -> RunH z t e r m a
ProcessH :: z a -> RunH z t e r m (t (Sem (e ': r)) a)
EmbedH :: t (Sem r) a -> RunH z t e r m a
interpretNew
:: forall e r a
=> (forall z t x. MonadTransControl t => e z x -> Sem (RunH z t e r ': r) x)
-> Sem r a -> Sem r a
then runReader
could be implemented as follows:
runReader i = interpretNew \case
Ask -> return i
Local f m -> do
m' <- processH m
embedH $ controlT $ \lower -> runReader (f i) (lower m')
Which is so complicated I'd prefer to save it for a rework of Tactics
.
-- ^ A function for attempting to see inside an @f@. This is no | ||
-- guarantees that such a thing will succeed (for example, | ||
-- 'Polysemy.Error.Error' might have 'Polysemy.Error.throw'n.) | ||
, weaveTrans :: forall n x. Monad n => (forall y. mAfter y -> n y) -> Sem rInitial x -> t n x |
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.
This is forall x. Sem rInitial x -> t m x
, but with t m
Yoneda-encoded.
This expresses the fact that Sem rInitial
can be rewritten as a stack of MonadTransControl
s of the current monad m
(this stack is expressed through the existential t
, which is a bunch of ComposeT
s of MonadTransControl
s corresponding to interpreters used).
The Yoneda encoding is to improve the efficiency of hoist
; if you represent t m
directly, then you would need to use hoistT
for every use of hoist
/weave
, which is ineffecient for some t
:s, like NonDetC
.
-- guarantees that such a thing will succeed (for example, | ||
-- 'Polysemy.Error.Error' might have 'Polysemy.Error.throw'n.) | ||
, weaveTrans :: forall n x. Monad n => (forall y. mAfter y -> n y) -> Sem rInitial x -> t n x | ||
, weaveLowering :: forall z x. Monad z => t z x -> z (StT t x) |
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.
This is the lowering function provided by a liftWith
, and corresponds to running a t z
under the initial state of the computation. So this corresponds to the initial state f ()
under the old weave
-based Weaving
.
-- ^ Even though @f a@ is the moral resulting type of 'Weaving', we | ||
-- can't expose that fact; such a thing would prevent 'Polysemy.Sem' | ||
-- from being a 'Monad'. | ||
, weaveInspect :: forall x. f x -> Maybe x |
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.
N.B. the inspector now implicitly exists by the fact that StT t
is Traversable
, so you can define:
inspect :: MonadTransControl t => StT t a -> Maybe a
inspect = foldr (const . Just) Nothing
type StT NonDetC = [] | ||
|
||
hoistT n nd = NonDetC $ \c b -> | ||
join $ n $ unNonDetC nd (\a r -> return $ c a (join (n r))) (return b) |
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.
Note: NonDetC
is not a well-behaved MonadTransControl
(due to #246), but this definition of hoistT
is well-behaved (morally, hoistT id == id
). This gives rise to an inconsistency, where:
controlT (\lower -> n (lower tm)) /= hoistT n tm
-- | An effect for running monadic actions within a higher-order effect | ||
-- currently being interpreted. | ||
newtype RunH z (m :: * -> *) a where | ||
RunH :: z a -> RunH z m a |
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 have a reason for not just reusing Embed
/embed
. Since z
is universally quantified in the handler passed to interpretNew
, if the handler tries to use, say, Embed IO
, then those uses will actually get stuck because GHC
can't prove that z
isn't IO
. This can be fixed by having embedding of higher-order thunks be a completely separate effect.
Besides, I don't like overloading Embed
that much. Having a separate effect for such a specific use-case as embedding higher-order thunks makes it easier for users to grok.
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.
does this mean that where you would use liftT
you now have to raise
or do you expect that to be mostly inferred?
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.
You'll need to use raise
when working with interpretNew
in two scenarios:
- You want to
send
a completely polymorphic effecte
inside the handler, since then GHC can't tell it's notRunH z
. - You want to bring actions that are arguments to the interpreter into the environment.
So for example, if you want to implement runOutputSem
using interpretNew
:
runOutputSem act = interpretNew \case
Output o -> raise (act o)
Otherwise, you shouldn't ever need to raise
. Indeed, most uses of interpret
can be replaced with interpretNew
and otherwise have the exact same definition and still work.
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.
awesome!
|
||
restoreT m = ComposeT (restoreT (restoreT (fmap getCompose m))) | ||
|
||
newtype Distrib f q m = Distrib (forall x. f (q x) -> m (f x)) |
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.
Hack: lets you bind the distribution function in a let
without the monomorphism restriction kicking in.
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.
filthy little monolocalbindses!
Although this doesn't introduce any breaking changes, we may want to do so anyway. For example, withWeavingToFinal
:: Member (Final m) r
=> (forall t. MonadTransControl t => (forall x. Sem r x -> t m x) -> t m a)
-> Sem r a However, I think such breaking changes should be done in a separate PR, since that's a much more difficult topic. |
Subsumed by #422. Closing, but feel free to open if you feel like it! |
This is the massive rework mentioned in #386 and #384 (comment).
This essentially switches
polysemy
from aweave
-based to aMonadTransControl
-based effect system, and miraculously does so without any breakage to any existing interface (outside of internal modules). This rewrite is done in order to support a new family of higher-order interpreter combinators -- currently calledinterpretNew
-- which let you run higher-order thunks through a simple embedding actionrunH
-- no state threading required!Note, though, that
MonadTransControl
is more or less equivalent toweave
, and this system still inherits all ofweave
's problems (except the difficulty of writing higher-order interpreters). So althoughpolysemy
wouldn't technically beweave
-based any longer, I'd still be calling itweave
-based since the difference is so small to the point of being irrelevant.This fixes #386.
Part of the rewrite is strengthening the
Tactical
environment such that the effectful state is represented by aTraversable
instead of aFunctor
. This is because you can expect the state of any well-behavedMonadTransControl
to beTraversable
(at the very least, every real-world example I've encountered is.) So this also fixes #367.