State is discarded inside bracket dealloc actions

[lexi-lambda]

Both these results seem wrong to me:

ghci> runM .@ runResource $ runState 0 $ bracket
        (pure ())
        (const (sendM . print =<< get @Integer))
        (const (put 2))
0
(2,())
ghci> runM .@ runResource $ runState 0 $ bracket
        (pure ())
        (const (put 2))
        (const (pure ()))
(0,())

It seems like it ought to be possible to fix this by using a custom version of bracket inside runResource that threads the state through appropriately, but if that’s necessary, then I suppose I’m a little confused about what makes the approach polysemy takes any better than MonadBaseControl with respect to dropping state.

[isovector]

Both of these seem wrong to me too; I'm sure that this used to work. Let me dive in and write some tests.

[isovector]

Nevermind, this is "expected behavior," for some definition of expected.

The type of base's bracket is bracket :: IO a -> (a -> IO b) -> (a -> IO c) -> IO c, which is pretty explicit that it's dropping the b. polysemy, fused-effects, and indeed all implementations based on "Effect Handlers in Scope" are going to have this same limitation, since they manipulate the return types to push state around.

There's a workaround, which is to use runStateInIORef.

[isovector]

To be more explicit about why this doesn't work, polysemy instantiates base's bracket at

bracket :: IO (s, a) -> ((s, a) -> IO (s, b)) -> ((s, a) -> IO (s, c)) -> IO (s, c)

which is why the c-scoped changes don't appear in the b-scope, and why the b-scope changes get ignored in the result.

[isovector]

In #73 we've been chatting about this problem more generally.

I think that in this particular case, the bug might just be a quirk of the runState interpretation of State --- "Note: this thing does not preserve state changes run outside of the main thread. Use runStateInIORef instead if you want those semantics."

Maybe it's a cop-out, but also maybe this is more of a documentation bug than anything else?

[ocharles]

Another bracket to consider is that in exceptions: https://hackage.haskell.org/package/exceptions-0.10.2/docs/Control-Monad-Catch.html#v:generalBracket

Maybe it's a cop-out, but also maybe this is more of a documentation bug than anything else?

This is a cop-out to me. This is a very real problem, and is half the reason that rio/unliftio exists: https://www.fpcomplete.com/blog/2017/06/tale-of-two-brackets

[isovector]

@ocharles thanks for the pointer to generalBracket. I forgot that I can just call mask explicitly. That gives us an explicit fix for #84, though not for the problem at large.

[isovector]

On second thought, even if we use get generlBracket into the same shape, we're still going to drop state changes that occur in the use block before a throw. I think IORefs are the only real solution here.

[isovector]

Discounting the above, generalBracket still isn't good enough to get us what we want, since we're left with a f b and an f c, at the end of the day, but we want to use the f from f b, but the c from f c. We can't do this with functors, but strengthening everything to an Applicative could make it work.

[ocharles]

It's worth slowing down, what is the behavior that we want? We can hardly strive to have correct behavior in polysemy if we don't have a goal! @lexi-lambda's original example seems to be essentially:

runStateT
  (bracketStateT
        (pure ())
        (const (sendM . print =<< get @Integer))
        (const (put 2)))
  0

Where bracketStateT :: StateT s IO a -> (a -> StateT s IO ()) -> (a -> StateT s IO b) -> StateT s IO b. So what should this program produce, and how would we write bracketStateT? I think only once we have that answer can we work out how this works in something more polymorphic.

[isovector]

I'd like

2
(2, ())

and

(2, ())

for the two examples, respectively.

In other news, the applicative idea above won't work, since we don't get the *> implementation we'd want for (,) s. There's nothing to stop us from packing a forall a b. f a -> f b -> f b inside of Yo, but I'm not convinced such a thing would compose with itself.

[isovector]

Responded to this discussion over to #73 in a better thought-out manner. I'm going to suggest we continue the chat there, since it makes sense to leave this ticket as a place to talk about the particular bug in question.

[isovector]

"Effect Handlers in Scope" points out the following:

• runError . runState has local-state semantics (relative to error)
• runState . runError has global-state semantics (relative to error)

It seems to me that this is the more fundamental problem here in #84. We don't have a place to runState underneath the Resource, and so we're restricted to the local-state semantics. This important detail of semantics is absolutely worth mentioning in runState, and I'm thinking through how to give a GlobalState effect that could be used to solve problems 1 and 2.

[lexi-lambda]

Sorry for opening this issue and disappearing. Something like generalBracket is, indeed, what I had in mind, but you’re right that pure (i.e. runState) state in the use action would still get discarded if an IO exception were raised.

[gelisam]

I suppose I’m a little confused about what makes the approach polysemy takes any better than MonadBaseControl with respect to dropping state.

My main problem with MonadBaseControl is that it is too easy to accidentally discard state. lifted-base's implementation of finally, for example, does not look particularly suspicious:

finally body sequel = control $ \runInIO ->
                        Base.finally (runInIO body)
                                     (runInIO sequel)

One needs to think carefully about the runtime behaviour of this implementation in order to realize that runInIO sequel produces a value of type StM m b representing the non-IO effects of sequel, and that since E.finally discards this value, those effects will be discarded.

With polysemy, however, the implementation does look suspicious:

data Finally m a where
  Finally :: m a -> m b -> Finally m a

runFinally :: forall r a. Member (Lift IO) r
           => (forall x. Sem r x -> IO x)
           -> Sem (Finally ': r) a
           -> Sem r a
runFinally finish = interpretH $ \case
  Finally body_ sequel_ -> do
    body   <- runT  body_
    sequel <- bindT (\() -> sequel_)
    
    let runInIO :: Sem (Finally ': r) x -> IO x
        runInIO = finish .@ runFinally

    fUnit <- getInitialStateT
    sendM $ Base.finally (runInIO body)
                         (runInIO $ sequel fUnit)

The getInitialStateT call tells us straight away that some non-IO effects are going to get discarded. Since sequel is given the initial state rather than the state returned by runInIO body, we know that sequel won't be able to see the non-IO effects performed in the body. I suspect runResource is implemented in a similar way, and that's why sendM . print =<< get @Integer prints the original state instead of the state set by put 2.

So, in my eyes, that's the advantage of polysemy over MonadBaseControl: when implementing an effect which discards state, you'll know that you are discarding the state, so you are more likely to mention the fact that the effects are discarded in your documentation. But for the users, the end result is the same: both implementations discard the state, that fact is not obvious from the types, and so we keep getting paper cuts while using those libraries. At least MonadBaseControl documents the fact that the effects get discarded!

[isovector]

@ocharles and I have a potential solution to this problem, which is to track the state functor f in the type system directly (rather than existentially), and to only allow runBracket when it is Identity.

[gelisam]

By the way, that's also the approach taken by MonadBaseControl: restricting some lifted functions to the safe case in which StM m ~ Identity, so there are no non-IO effects to discard.

[gelisam]

I suspect runResource is implemented in a similar way, and that's why sendM . print =<< get @Integer prints the original state instead of the state set by put 2.

Surprisingly, this is not the case: runResource does not call getInitialStateT!

Bracket alloc_ dealloc_ use_ -> do
  alloc   <- runT  alloc_
  dealloc <- bindT dealloc_
  use     <- bindT use_

  let runInIO :: Sem (Resource ': r) x -> IO x
      runInIO = finish .@ runResourceInIO_b

  sendM $ Base.bracket (runInIO alloc) (runInIO . dealloc) (runInIO . use)

It turns out there are two different ways in which lifted-base's finally is dropping non-IO effects, and polysemy is only making one of them obvious, and only some of the time.

1. the non-IO effects occurring inside sequel are not visible after finally body sequel (because Base.finally discards the result of its second argument)
2. the non-IO effects occurring inside body are not visible inside sequel (because runInIO restores the state captured by control before finally body sequel begins)

The fact that (1) is happening is just as hard to see in the polysemy implementation as in the MonadBaseControl implementation. Polysemy makes (2) obvious in some circumstances, by forcing the implementation to call getInitialStateT. But runResource above suffers from both (1) and (2), even though it does not call getInitialStateT! What's going on?

The runT/bindT/bindT/... idiom adds a bunch of fs which hold the state:

foo_ :: m a
bar_ :: a -> m a
baz_ :: a -> m a

foo <- runT  foo_
bar <- bindT bar_
baz <- bindT baz_

foo :: m (f a)
bar :: f a -> m (f a)
baz :: f a -> m (f a)

Then, in

do fa   <- foo
   fa'  <- bar fa
   fa'' <- baz fa'
   pure fa''

That f is threaded through, so that bar can see the effects of foo, baz can see the effects of the first two, and the caller can see the effects of all three. This is what we want. But in

do fa  <- foo
   fa' <- bar fa
   _   <- baz fa
   pure fa'

the f is threaded in such a way that baz cannot see the effects of bar and the caller cannot see the effects of baz, causing those effects to be dropped. This is what is happening in runResource: Base.bracket is sending the output of alloc to both use and dealloc, and then returns the f a returned by use, thereby discarding the effects produced by dealloc.

Perhaps it would be worth making the runT/bindT/bindT/... idiom more constrained, so that each function produces a value which can only be accepted by the next function in the list?

foo <- runT  foo_
bar <- bindT bar_
baz <- bindT baz_

foo :: m (f a)
bar :: f a -> m (g a)
baz :: g a -> m (h a)

I realize, however, that this goes in the opposite of the direction you want to explore, in which the f a is made more transparent rather than more opaque, so you can extract the a or require f to be Identity.

[isovector]

Perhaps it would be worth making the runT/bindT/bindT/... idiom more constrained, so that each function produces a value which can only be accepted by the next function in the list?

How would you write bracket, in which you want to fork two continuations off of the alloc?

[gelisam]

How would you write bracket, in which you want to fork two continuations off of the alloc?

In the same way getInitialStateT makes it very clear that you're only allowing one of the steps to see the state as it was at the very beginning of the action, there would be a more general piece of machinery making it very clear that you're allowing one of the steps to see the state as it was at some prior state. To write the type of that function, I first need to switch my notation from consecutive letters f, g, h to type-level naturals F f 1, F f 2, F f 3:

foo :: m (F f 1 a)
bar :: f 1 a -> m (F f 2 a)
baz :: f 2 a -> m (F f 3 a)

The caller is supposed to see all of the effects, so we'd somehow need to keep track of the highest number (in this case 3) and ask the interpreter to return that:

returnF :: forall x. F f 3 x -> Tactic ... (f x)

All right, now the happy case in which no effects get dropped looks like this:

do f1a <- foo
   f2a <- bar f1a
   f3a <- baz f2a
   returnF f3a

And the case in which some of the effects are dropped looks like this:

skipEffects :: forall x. F f n x -> F f (n + 1) x

do f1a <- foo
   f2a <- bar f1a
   _   <- baz (skipEffects f1a)
   returnF (skipEffects f2a)

Our piece of machinery is skipEffects, and it makes it very clear that baz cannot see the effects of bar and that the caller cannot see the effects of baz.

As requested, here's how we can write bracket using that API:

import GHC.TypeLits
import Polysemy
import qualified Control.Exception as Base

newtype F f (n :: Nat) a = F { unF :: f a }

skipEffects :: F f n x -> F f (n + 1) x
skipEffects = F . unF


data Resource m a where
  Bracket :: m a -> (a -> m c) -> (a -> m b) -> Resource m b

makeSem ''Resource

runResourceInIO :: forall r a. Member (Lift IO) r
                => (forall x. Sem r x -> IO x)
                -> Sem (Resource ': r) a
                -> Sem r a
runResourceInIO finish = interpretH $ \case
    Bracket alloc__ dealloc__ use__ -> go alloc__ dealloc__ use__
  where
    go :: forall f m a b c
        . m a
       -> (a -> m c)
       -> (a -> m b)
       -> Sem (WithTactics Resource f m r) (f b)
    go alloc__ dealloc__ use__ = do
      alloc_   <- runT  alloc__
      use_     <- bindT use__
      dealloc_ <- bindT dealloc__

      let alloc :: Sem (Resource ': r) (F f 1 a)
          alloc = fmap F alloc_

          use :: F f 1 a -> Sem (Resource ': r) (F f 2 b)
          use = fmap F . use_ . unF

          dealloc :: F f 2 a -> Sem (Resource ': r) (F f 3 c)
          dealloc = fmap F . dealloc_ . unF

          returnF :: forall x. F f 3 x -> Sem (WithTactics Resource f m r) (f x)
          returnF = return . unF

          runInIO :: Sem (Resource ': r) x -> IO x
          runInIO = finish .@ runResourceInIO

      f2b <- sendM $ Base.bracket
        (runInIO alloc)
        (runInIO . dealloc . skipEffects)
        (runInIO . use)

      let f3b :: F f 3 b
          f3b = skipEffects f2b
      returnF f3b

It should now be obvious from the skipEffects calls that with this implementation, dealloc does not see the effects of use (which is why in the first example, sendM . print =<< get @Integer prints 0 despite use's put 2), and that the caller does not see the effects of dealloc (which is why in the second example, the overall result is (0,()) despite dealloc's put 2).

I think an implementation based on generalBracket would drop fewer effects, but would still drop the effects of use if use throws an exception.

[isovector]

This would be fixed by #126

[ocharles]

@gelisam I've only skimmed your comment, but it looks very similar to what's going on in Syntax and Semantics for Operations with Scopes - is it the same thing?

[gelisam]

@ocharles No, I don’t see any link between that paper and any of my comments. I am guessing that the similarity you noticed is that we both use type-level natural numbers in relation to an interpreter, but we use them in completely different ways.

For the benefit of others who are following this thread, here is a summary of the paper.

I don't think the formalism used in the paper is able to represent the type of bracket :: m a -> (a -> m c) -> (a -> m b) -> m b, so let's simplify to bracket_ :: m a -> m a -> m a -> m a, where the as returned by the acquire and release actions are ignored. This operation is "non-algebraic", in the sense that bracket_ acquire release body >>= f is not the same as bracket_ (acquire >>= f) (release >>= f) (body >>= f).

The reason algebraicity matters is that we need a way to represent programs containing bracket_ calls. With an algebraic operation like trace :: String -> m a -> m a, we can use Free Op to represent programs containing trace calls, using a constructor Trace :: String -> a -> Op a. Such a representation supports monadic composition, by nesting sub-trees. But if we define a constructor Bracket_ :: a -> a -> a -> Op a, nesting sub-trees will have the wrong effect, it will simply make the acquire, release and body arguments larger.

To solve this problem, the key idea is that acquire, release and body need to contain a special delimiter separating the part of acquire, release and body which was originally given to bracket_ from the (>>= f) which later gets concatenated. Assuming we have such a delimiter, we can now define a helper operation bracketOpen :: m a -> m a -> m a -> m a whose semantics are defined in terms of that delimiter. We'll call the delimiter close, the idea being that bracketOpen opens a scope in all three of its arguments, and that the close delimiter closes them. The semantics we'll give to bracketOpen acquire release body is that it runs acquire until the matching close, ignoring the rest, then it runs body until the matching close, keeping the rest for later, then it runs release until the matching close, ignoring the rest, and finally runs the rest of body. We can now define bracket_ acquire release body = bracketOpen (acquire <* close) (release <* close) (body <* close). With this new semantics, bracket_ acquire release body >>= f is now the same as bracket_ (acquire >>= f) (release >>= f) (body >>= f), so we've managed to make bracket_ algebraic!

That's neat, but polysemy's Yo representation is already able to represent non-algebraic effects, and Yo even supports effects like bracket :: m a -> (a -> m c) -> (a -> m b) -> m b which have a complicated type. And we haven't reached the part with the type-level naturals yet.

Those type-level naturals come from the fact that the open and close operations and delimiters can nest arbitrarily deep, and so the naturals track how deeply-nested the code is. More precisely, an interpreter may choose to interpret blocks of code at different depths to different types, which it may specify by defining a type family Output :: Nat -> *. Then, since the inputs of an open operation are more nested than that operation itself, the interpreter must supply a function from Op (Output (S n)) to Output n. And since the code after a closing delimiter is less nested than the code before it, the interpreter must also supply a function from Output n to Output (S n).

As you can see, the paper uses type-level naturals in a completely different way than I am. They are requiring the interpreter to choose a type family and to implement functions on that type family, whereas I am proposing to provide the interpreter with an opaque type family and to provide the interpreter with a few functions on that type family. Furthermore, all the inputs of their open operation have the same type-level number, namely one more than the open operation itself, whereas I am proposing that they should have different numbers in order to enforce that the output of one is fed as the input of the next.

[ocharles]

Thanks @gelisam - that was exactly my question.