polysemy-research / polysemy

:gemini: higher-order, no-boilerplate monads
BSD 3-Clause "New" or "Revised" License
1.04k stars 72 forks source link

Restrict placement of transformative interpreters #259

Open KingoftheHomeless opened 4 years ago

KingoftheHomeless commented 4 years ago

Transformative interpreters - which interpret effects in terms of other effects in the effect stack - circumvent the usual rule-of-thumb that the semantics of how effects interact depend on the order interpreters are used, and therefore, in what order effects appear in the stack.

The most common use of such transformative interpreters are those that target Embed IO or Final IO, which is why many of these have Beware s attached to them.

Ideally, we would be able to restrict the use of transformative interpreters such that they can't be used in scenarios where the rule-of-thumb would be violated, without otherwise compromising how they may be used.

The alternative to doing this is making it clearly understood that the order of effects is only a soft constraint on local/global state semantics, and that transformative interpreters violate it. This is far from ideal, as having effect ordering dictate local/global state semantics would be a very, very nice property to have; it would allow us to use constraints like those #254 introduces without having to worry about it.

I've detailed the most promising (but yet woefully inadequate) solution I've yet managed to find here: https://github.com/polysemy-research/polysemy/issues/259#issuecomment-543845832.

KingoftheHomeless commented 4 years ago

The fact that Ctrl-Enter immediately opens the issue you're working on continues to drive me insane.

KingoftheHomeless commented 4 years ago

The most promising solution I've found yet is to have transformative interpreters force the targeted effect to appear just before the interpreted effect, like this:

asyncToIOFinal
  :: Sem (Final IO ': Async ': r) a
  -> Sem (Final IO ': r) a

errorToIOFinal
  :: Typeable e
  => Sem (Final IO ': Error e ': r) a
  -> Sem (Final IO ': r) (Either e a)

writerToIOFinal
  :: Monoid o
  => Sem (Final IO ': Writer o ': r) a
  -> Sem (Final IO ': r) (s, a)

Although the types are clunky, the effect of this is that once you use any transformative interpreter to an effect A, you are restricted to only using other transformative interpreters to A up until the point you interpret A.

For example, this would compile:

ex :: IO ([Int], Either String ())
ex =
    runFinal
  . writerToIOFinal
  . errorToIOFinal
  . asyncToIOFinal
  $ ...

while this would not:

ex :: IO ([Int], Either String ())
ex =
    runFinal
  . runWriter -- runWriter would cause Writer to have local state semantics with regards to Error and Async
  . errorToIOFinal
  . asyncToIOFinal
  $ ...

The issue with this solution is the interplay with Embed IO and Final IO; we would like outputToIOMonoid to have the following type:

outputToIOMonoid
  :: Monoid s
  => (o -> s)
  -> Sem (Embed IO ': Output o ': r) a
  -> Sem (Embed IO ': r) (s, a)

But now outputToIOMonoid can't be used freely in conjunction with transformative interpreters to Final IO, even though there should be no issue in doing so:

-- this wouldn't compile
ex :: IO ([Int], Either String ())
ex =
    runFinal
  . outputToIOMonoid id
  . errorToIOFinal
  . asyncToIOFinal
  $ ...

This can be mitigated by separating the effects that use Embed IO with the effects that use Final IO through the use of embedToFinal, like this:

ex :: IO (Either String ([Int], ()))
ex =
    runFinal
  . errorToIOFinal
  . asyncToIOFinal
  . embedToFinal
  . outputToIOMonoid id
  $ ...

But this is a horrible idea for several reasons:

  1. There's no reason to force that interpreters that use Embed IO come before interpreters that use Final IO. In fact, in this case, it's forces us to have the resulting tuple of outputToIOMonoid be hidden inside the Either that errorToIOFinal creates, even though outputToIOMonoid uses a IORef, and thus outputs should in reality never be lost.
  2. We're looking at replacing runFinal and embedToFinal with a common interpreter for both Embed and Final: runM :: Monad m => Sem '[Embed m, Final m] a -> m a. This would make that change impossible.
  3. This is a solution for Embed m and Final m, but there might be other scenarios where we would like transformative interpreters with different target effects to be used in conjunction with eachother.

A fix to 1. would be to introduce the following (with a snappier name):

class Embedder e where
  liftEmbed :: (Member (e m) r, Monad m) => m a -> Sem r a 

and then have outputToIOMonoid have the following signature instead:

outputToIOMonoid
  :: (Monoid s, Embedder e)
  => (o -> s)
  -> Sem (e IO ': Output o ': r) a
  -> Sem (e IO ': r) (s, a)

Since both Embed and Final can have instances of Embedder. This doesn't fix 2. or 3. though.