Skip to content
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

Closed
wants to merge 4 commits into from

Conversation

KingoftheHomeless
Copy link
Collaborator

@KingoftheHomeless KingoftheHomeless commented Dec 18, 2020

This is the massive rework mentioned in #386 and #384 (comment).

This essentially switches polysemy from a weave-based to a MonadTransControl-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 called interpretNew -- which let you run higher-order thunks through a simple embedding action runH -- no state threading required!

Note, though, that MonadTransControl is more or less equivalent to weave, and this system still inherits all of weave's problems (except the difficulty of writing higher-order interpreters). So although polysemy wouldn't technically be weave-based any longer, I'd still be calling it weave-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 a Traversable instead of a Functor. This is because you can expect the state of any well-behaved MonadTransControl to be Traversable (at the very least, every real-world example I've encountered is.) So this also fixes #367.

src/Polysemy.hs Outdated Show resolved Hide resolved
--
-- @since TODO
interpretNew :: forall e r a
. (forall z x. e z x -> Sem (RunH z ': r) x)
Copy link
Collaborator Author

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

Copy link
Member

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?

Copy link
Collaborator Author

@KingoftheHomeless KingoftheHomeless Dec 19, 2020

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
Copy link
Collaborator Author

@KingoftheHomeless KingoftheHomeless Dec 19, 2020

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 MonadTransControls of the current monad m (this stack is expressed through the existential t, which is a bunch of ComposeTs of MonadTransControls 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)
Copy link
Collaborator Author

@KingoftheHomeless KingoftheHomeless Dec 19, 2020

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
Copy link
Collaborator Author

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)
Copy link
Collaborator Author

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
Copy link
Collaborator Author

@KingoftheHomeless KingoftheHomeless Dec 19, 2020

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.

Copy link
Member

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?

Copy link
Collaborator Author

@KingoftheHomeless KingoftheHomeless Dec 19, 2020

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 effect e inside the handler, since then GHC can't tell it's not RunH 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.

Copy link
Member

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))
Copy link
Collaborator Author

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

filthy little monolocalbindses!

@KingoftheHomeless
Copy link
Collaborator Author

Although this doesn't introduce any breaking changes, we may want to do so anyway. For example, Final can be revamped to have the following be the new withWeavingToFinal:

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.

src/Polysemy.hs Outdated Show resolved Hide resolved
@isovector
Copy link
Member

Subsumed by #422. Closing, but feel free to open if you feel like it!

@isovector isovector closed this Oct 19, 2021
@tek tek deleted the core-rewrite branch September 23, 2023 12:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Revamp interpretH Can the Tactical Functor be Traversable?
4 participants