Restrict the existentially quantified monad in a Weaving to be Sem r

[KingoftheHomeless]

From the documentation for Weaving in Polysemy.Internal.Union:

data Weaving e m a where
  Weaving
    :: Functor f
    =>   { weaveEffect :: e m a
         -- ^ The original effect GADT originally lifted via
         -- 'Polysemy.Internal.send'. There is an invariant that @m ~ Sem r0@,
         -- where @r0@ is the effect row that was in scope when this 'Weaving'
         -- was originally created.
             ...
         }
    -> Weaving e n b

Turns out that knowing that m ~ Sem r0 can actually be relevant, since that means m is a monad, and that allows you to manipulate actions that you transform using the distribution weaveDistrib :: forall x. f (m x) -> n (f x).

For a toy example, it would allow interpreting effects like these (which is not possible today):

data Zip m a where
  Zip :: m a -> m b -> Zip m (a, b)

Through the following:

runZip :: Sem (Zip ': r) a -> Sem r a
runZip = interpretH $ \case
  Zip ma mb -> do
    mab <- runT (liftA2 (,) ma mb) -- Requires knowing that existential monad is truly a monad
    (raise . runZip) mab

For a more convincing example, this would allow us to write the following interpreter:

newtype Restoration m = Restoration (forall x. m x -> m x)

maskToFinal
  :: (Member (Final m) r, MonadMask m)
  => Sem (Mask (Restoration m) ': r) a
  -> Sem r a

For the following effect, which completely encapsulates the power of the MonadMask type-class:

data Mask s m a where
  Mask' :: (s -> m a) -> Mask s m a
  UninterruptibleMask' :: (s -> m a) -> Mask s m a
  Restore' :: s -> m a -> Mask s m a
  GeneralBracket ::
       m a
    -> (a -> ExitCase b -> m c)
    -> (a -> m b)
    -> Mask s m (b, c)

To be more specific, this change allows for the interpretation of GeneralBracket in a similar way as in polysemy-research/polysemy-zoo#61.

We want to change Weaving as follows:

data Weaving e m a where
  Weaving
    :: Functor f
    =>   { weaveEffect :: e (Sem r0) a
         -- ^ The original effect GADT originally lifted via
         -- 'Polysemy.Internal.send'.
         -- @r@ is the effect row that was in scope when this 'Weaving'
         -- was originally created.
             ...
       , weaveDistrib :: forall x. f (Sem r0 x) -> m (f x)
         -- ^ Distribute @f@ by transforming @Sem r0@ into @m@. We have invariants
         -- on @Sem r0@ and @m@, which means in actuality this function (typically) 
         -- looks like
         -- @f ('Polysemy.Sem' (Some ': Effects ': r) x) -> 'Polysemy.Sem' r (f
         -- x)@.
             ...
         }
    -> Weaving e m b

Part of the incurred refactoring is trivial:
The type signatures of inj/Using needs to be updated.

We need to modify combinators that (re)interpret/intercept effects such that they may make use of the fact that m ~ Sem r.
For example, interpretFinal should have its type signature changed to:

interpretFinal
    :: forall m e r a
     . Member (Final m) r
    => (forall x r0. e (Sem r0) x -> Strategic m (Sem r0) x)
       -- ^ A natural transformation from the handled effect to the final monad.
    -> Sem (e ': r) a
    -> Sem r a

Here's a list:

• interpret/H
• intercept/Using/H
• reinterpret/2/3/H
• rewrite
• transform

The greatest problem with this change is that it causes Polysemy.Internal and Polysemy.Internal.Union to become mutually recursive, which can't be trivially fixed. One way to fix this is to move the definition of Sem r (and its instances) into Polysemy.Internal.Union, but is that really what we want? I'd love help/opinions on how to address this.
Just use this as Polysemy/Internal.hs-boot:

{-# LANGUAGE RoleAnnotations #-}
module Polysemy.Internal where

import Polysemy.Internal.Kind

type role Sem nominal nominal
data Sem (r :: EffectRow) (a :: *)

instance Functor (Sem r)
instance Applicative (Sem r)
instance Monad (Sem r)

and stick an import {-# SOURCE #-} Polysemy.Internal into Polysemy.Internal.Union.

There are several alternatives to implementing this change:

1. Instead of restricting the existentially quantified monad to be Sem r, restrict it to be an arbitrary monad.
   This neatly side-steps the issue of mutually recursive modules, but also means that Weaving will also carry around a Monad dictionary. The performance impact of this is most likely unacceptable.

2. Instead of restricting m to be Sem r in the Weaving, have the effect do it.
   For example, Zip can instead be defined as follows:

data Zip m a where
  Zip :: Sem r a -> Sem r b -> Zip (Sem r) (a, b)

Which will prove that the existentially quantified monad is Sem r upon pattern matching on Zip.
This works, but needing the effect to specify that m ~ Sem r strikes me as ugly.
You can also conjure a semi-plausible scenario in which you'd like to create an interpreter for a higher-order effect that doesn't belong to you, but the interpreter you'd like to define needs to know that m ~ Sem r and the effect doesn't place that restriction.

[ocharles]

Your alternatives don't consider a hs-boot file - would you be open to that? Other than that, I'd just move Union and Sem to Polysem.Internal.Sem

[TheMatten]

So we would just keep weaveDistrib :: forall x. f (m x) -> n (f x) as it is?

[KingoftheHomeless]

I did try to implement a .hs-boot file, but gave up on it since the definitions of Sem and Weaving are mutually recursive, and I figured there was no way around that. Turns out I was wrong, since you don't actually need to specify the definitions of the data types.

So yes, this is fixable by using the following as Polysemy/Internal.hs-boot:

{-# LANGUAGE RoleAnnotations #-}
module Polysemy.Internal where

import Polysemy.Internal.Kind

type role Sem nominal nominal
data Sem (r :: EffectRow) (a :: *)

instance Functor (Sem r)
instance Applicative (Sem r)
instance Monad (Sem r)

And then sticking a import {-# SOURCE #-} Polysemy.Internal in Polysemy.Internal.Union.

@TheMatten No, m should be replaced with Sem r0 there. Good catch!

[TheMatten]

I'm wondering - is m in Weaving e m a always of shape Sem r too? We could then change middle argument to instead contain row (r) and have n be Sem r. And remove m completely from Union it seems?

[KingoftheHomeless]

It doesn't have to be, but the weaving can really only be used once it is.

Nevertheless, I'd hold off on removing the m parameter. Unlike the existential variable, there's no real benefit to specializing it.

Edit: If you're suggesting Union r m a to be changed to Union r a, that won't work. For one thing, decomp will break. Sometimes the effect row of the union and the effect row of the Union's Sem differ.

[TheMatten]

@KingoftheHomeless Ah, there's e.g. weaken - yeah, you're right.

[A1kmm]

I did an experiment to see if it is possible to restrict Weaving to force m to be Sem r0 over here: https://github.com/polysemy-research/polysemy/compare/master...A1kmm:weaving-sem-experiment?expand=1

It doesn't work because the documented invariant about m is not actually always true. For example, in

polysemy/src/Polysemy/Internal/Writer.hs

Line 201 in 016c16f

=> (forall m x. Monad m => Weaving e (Lazy.WriterT o m) x -> Lazy.WriterT o m x)

, m = Lazy.WriterT o m, so not a Sem. Similarly for State, where m = S.StateT s (Sem r').

I think this brings into question the whole premise of this issue, and maybe something like #328 is a more workable approach.

[KingoftheHomeless]

The existentially quantified monad in a Weaving does not refer to the m of the type Weaving e m a, but rather, the m in the constructor Weaving :: Functor f => { weaveEffect :: e m a, ... } -> Weaving e n b I'm sorry about the confusion, especially since you have put a lot effort in your fork based on it...

Locking this "inner", invisible-to-the-outside-world m to Sem r0, where r0 is also existential, wouldn't cause any complications outside of those mentioned in the OP. You wouldn't need to modify interpretViaLazyWriter.

If you're interested in carrying on, use the changed definition of Weaving as specified in OP, and go from there. Note that weaveEffect, weaveDistrib, and the return type of the constructor are modified.
Otherwise, I'll do this as part of the work for v2.0, which I will work full-time on once I don't have to worry about my studies.

[A1kmm]

Good point - we don't need to change both monad parameters.

I had a go at only changing mBefore (to use the terminology I introduced in the lower commits of my branch), which is the existentially quantified parameter in the Weaving constructor. I tried modifying the top commit of my change like this: A1kmm@c76424e.

It still runs into problems with definitions like https://github.com/A1kmm/polysemy/blob/c76424e326f10ada3f7623dc2b79989b38cce6a0/src/Polysemy/State.hs#L255.

In that code, weaveDistrib = \(s', m') -> fmap swap $ S.runStateT m' s', which has to fit into weaveDistrib :: forall x. f (Sem rBefore x) -> mAfter (f x), where type f a = (s, a), so weaveDistrib :: forall x. (s, Sem rBefore x) -> mAfter ((s, x)). But runStateT expects a StateT m x, so at least hoistStateIntoStateT isn't going to work unmodified with that constructor definition.

[A1kmm]

It turns out the above problem was only because I made weave and hoist unnecessarily weak. When I fixed that issue, the existing definition of hoistStateIntoStateT continues to compile.

I have squashed all my changes into one commit (original series of commits still available here: https://github.com/polysemy-research/polysemy/compare/master...A1kmm:weavingdetails-sem-experiment?expand=1), and made PR #333.

[KingoftheHomeless]

This has been addressed by #333.