instance MonadUnliftIO Ctl

[arybczak]

Can it be written? :thinking:

[re-xyr]

(I assume you mean speff-same-scope; the other two branches speff and speff-no-io are abandoned)

No - because you'd need Ctl a -> IO a:

instance MonadUnliftIO Ctl where
  withRunInIO f = Ctl $ fmap Pure $ f \(Ctl m) -> _what

MonadBaseControl is possible though:

instance MonadBaseControl IO Ctl where
  type StM Ctl a = Result a
  liftBaseWith f = Ctl $ fmap Pure $ f unCtl
  restoreM = Ctl . pure

though I'd rather not have it because it certainly would cause all kinds of semantic problems.

[arybczak]

(I assume you mean speff-same-scope; the other two branches speff and speff-no-io are abandoned)

No - because you'd need Ctl a -> IO a:

instance MonadUnliftIO Ctl where
  withRunInIO f = Ctl $ fmap Pure $ f \(Ctl m) -> _what

Right. That's what I thought :( That makes it unviable for real-world usage to me.

MonadBaseControl is possible though:

instance MonadBaseControl IO Ctl where
  type StM Ctl a = Result a
  liftBaseWith f = Ctl $ fmap Pure $ f unCtl
  restoreM = Ctl . pure

though I'd rather not have it because it certainly would cause all kinds of semantic problems.

True, if the yield or raise can be lost, we're back to square one.

Ok, thanks for exploring this area. I have a feeling that if/when proper support for delimited continuations in merged into GHC, this shouldn't be a problem anymore since with the low-level support you can manipulate the call stack and effectively bypass the type system, so it should be possible to write MonadUnliftIO Eff even when delimited continuations are used underneath.

I'm wondering about this since while I don't personally need the NonDet effect, it would be nice to be able to have proper support for it in effectful / cleff. I'm much less convinced about providing support for coroutines, since:

1. In other languages they are usually treated as very low level primitives and used as implementation detail for other control mechanisms.

2. They (as demostrated by eff) unlock a can of worms that makes it very hard to reason what will happen, how and where, while preventing these interactions from being able to wreck your world seems to be problematic.

cc @lexi-lambda - my current assumption is that once your patch for delimited continuations is merged, effectful and cleff can use it to support NonDet somewhat "for free", i.e. without compromising existing guarantees and functionality of these libraries (in particular, the existence of MonadUnliftIO instance). The Coroutine effect still remains an open question to me.

[re-xyr]

Alexis and I discussed the Coroutine problem last time. From what I understood, we don't want the resumption to escape the scope of control specifically because of this one interaction:

interpret[1] { DoThenAbort m -> do { m ; abort () } }
  interpret[2] { Quit -> control \k -> pure k }
    do { DoThenAbort $ do { Quit } }

--> [Instantiates DoThenAbort]

interpret[1] { DoThenAbort m -> do { m ; abort () } }
  interpret[2] { Quit -> control \k -> pure k }
    do { Quit; abort[1] () }

--> [Instantiates Quit]

interpret[1] { DoThenAbort m -> do { m ; abort () } }
  interpret[2] { Quit -> control \k -> pure k }
    do { control[2] \k -> pure k; abort[1] () }

--> [control]

interpret[1] { DoThenAbort m -> do { m ; abort () } }
  pure \x -> interpret[2] { Quit -> control \k -> pure k }
    do { pure x; abort[1] () }

--> [The result is a pure value by this point; eliminate interpret[1]]

pure \x -> interpret[2] { Quit -> control \k -> pure k }
  do { pure x; abort[1] () }

at which point you get an abort without a pairing interpret. the pseudocode is a bit handwavy, but you get the point.

In other words, the interaction of

• You can still control/abort after embedding an esSend computation in a handler
• Continuations can escape the scope of control

means the esSend computation can capture a resumption with your abort in it, escape the scope with that resumption, making that abort not have its pairing interpret. On the other hand, the removal of either functionality avoids this problem. This is all speculation though, I haven't proved it.

[re-xyr]

@arybczak Note that IO-native prompt and control doesn't "just work" in all scenarios; particularly, they won't be able to penetrate forkIOs - i.e. this won't work:

prompt tag $ do
  forkIO $ do
    ...
    control tag ...

-- GHC.Exts.control0#: no matching prompt in the current continuation

...which is a good thing because such behavior can't possibly be well defined, but also a bad thing because we haven't really figured out how to rule them out in an effect system.

One way could be to only allow embedding first-order IO computations, but this also rules out "good" higher-order IO functions that do not switch threads, like catch. The only other way I can think of now is to slap big warning signs all over the docs.

[arybczak]

Ideally I'd like to use prompt and control just for NonDet and leave everything else as-is, so Error would still use exceptions underneath.

So this would only be a problem if someone spawns threads inside the NonDet effect. IIUC the implementation should throw an exception if control cannot find a matching prompt, but even if it can't, since in effectful Env is thread-local, maybe I can keep track of active prompts in Env directly and detect this particular case to present an user friendly error. On the other hand, I also don't know how delimited continuations will cooperate with mutable Env.

My understanding of delimited continuations is still shallow at best, so this all might not work the way I think it does.

[re-xyr]

Yes, I think that kind of check is possible. When an effect is handled, you can just put the current ThreadId together with the PromptTag in the Env, and check if you're still on the same thread when you yield. But this is still a dynamic check - it'll be better if we can come up with a static one.

Also this check doesn't help us deal with when the user insists to unlift an unsafePerformIO/unsafeInterleaveIO call with a control inside - although that usage is probably much less justifiable.

Regarding mutable Env, I don't think control is clever enough to automatically rollback that for you - so you might want to cloneEnv once for each continuation call.

[re-xyr]

On another note, embedding catch may also be problematic. This is because if we need control0, or for the resumption to escape the scope of the handler, the capture will need to be bubbled up with throws. If the user is able to embed a catch @SomeException then they effectively intercept this capture and interrupts the control flow. (I believe this is a flaw of GHC.)

If we only enable controls and only allow the resumptions to be called locally, then maybe there won't be this problem? ...

[arybczak]

FYI, I experimented with delimited continuations since https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7942 was merged and I'm slightly confused. I got the basic version of the NonDet working, but I'm clearly missing something.

Consider this:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
{-# OPTIONS_GHC -Wall #-}
module Main where

import Control.Applicative
import Control.Exception
import Data.IORef
import GHC.Exts
import GHC.IO

main :: IO ()
main = do
  v <- newIORef (0::Int)
  r <- runNonDet @[] $ \tag -> do
    bracket_ (modifyIORef' v succ) (modifyIORef' v pred) $ do
      x <- choose tag (pure True) (pure False)
      y <- choose tag (pure 'a')  (pure 'b')
      pure (x, y)
  putStrLn $ "r: " ++ show r
  putStrLn . ("v: " ++) . show =<< readIORef v

----------------------------------------

runNonDet :: Alternative f => (PromptTag (f r) -> IO r) -> IO (f r)
runNonDet f = do
  tag <- newPromptTag
  prompt tag (pure <$> f tag)

choose :: Alternative f => PromptTag (f r) -> IO a -> IO a -> IO a
choose tag ma mb = control0 tag $ \k -> do
  fa <- prompt tag $ k ma
  fb <- prompt tag $ k mb
  pure $ fa <|> fb

----------------------------------------

data PromptTag a = PromptTag (PromptTag# a)

newPromptTag :: IO (PromptTag a)
newPromptTag = IO $ \s -> case newPromptTag# s of
  (# s', tag #) -> (# s', PromptTag tag #)

prompt :: PromptTag a -> IO a -> IO a
prompt (PromptTag tag) (IO m) = IO $ prompt# tag m

control0 :: PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b
control0 (PromptTag tag) f =
  IO . control0# tag $ \k -> case f $ \(IO a) -> IO (k a) of IO b -> b

and it kinda works, but not quite as I would expect it to. It produces

r: [(True,'a'),(True,'b'),(False,'a'),(False,'b')]
v: -3

So you get multiple results, but there is a problem with bracket - the finishing action runs 4 times as I'd expect it to, but the starting action runs only once!

Which I find confusing, because the prompt delimits the whole bracket, so captured continuation should include modifyIORef' v succ, but for a reason I don't understand it doesn't and I don't know how to make it do that.

[re-xyr]

I believe the continuation only captures everything from the control call till the end of the prompt. It is possible that this will lead to some confusing behavior though (not limited to bracket), but I don't think we can do anything specific for this except to inform users of this semantics and warn them against using IO unlifting in conjunction with potentially non-tail-resumptive effects.

[lexi-lambda]

Please read the documentation for those primops before using them—using them with arbitrary IO code is not safe.

[re-xyr]

I believe bracket is well-behaved wrt control0#; it doesn't violate any of the primop's invariants, and specifically the docs says it is possible to use masking functions with control0# - it's just the resulting semantics is not what he expected.

---

@arybczak In fact, in the NonDet + Writer section of the effect semantics zoo, you can see a justification for the semantics: https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md#nondet--writer

[lexi-lambda]

I believe bracket is well-behaved wrt control0#

No, it is not. A version of bracket that was designed to support delimited continuations would act like Scheme’s dynamic-wind, which the docs explicitly note is not provided by GHC. bracket only deals with upward jumps triggered by an exception, so using control0# with code that uses bracket (without any additional protections in place) will leak resources.

[re-xyr]

Well, that's true! I only meant that using bracket will not corrupt the runtime or cause a runtime exception on itself, but surely, it no longer follows its intended semantics.

[arybczak]

I believe the continuation only captures everything from the control call till the end of the prompt

I see, that makes sense.

Please read the documentation for those primops before using them—using them with arbitrary IO code is not safe.

I did read it (though can't say the same about fully understanding it apparently).

The program I included is a simplification of the program from your semantics-zoo:

action :: (NonDet :< es, Writer (Sum Int) :< es) => Eff es ((Sum Int), Bool)
action = listen (add 1 *> (add 2 $> True <|> add 3 $> False))
  where add = tell . Sum @Int

main :: IO ()
main = do
  print $ run (runNonDetAll @[] $ runWriter @(Sum Int) action)

The problem I had when I tried to translate it to effectful was that runWriter in effectful is essentially a bracket that pushes and takes off a handler from the stack of effects. So when action is executed, it'll just not work at all, because after the first branch finishes, the handler is no longer there.

But even if it didn't use bracket (like cleff afaik), it would use the same listen in both branches, so it wouldn't behave "nicely" anyway, i.e. it would have semantics of mtl + pipes.

I was hoping both cleff and effectful could just use delimited continuations for NonDet and require no other significant changes, but apparently that is not the case :disappointed:

[lexi-lambda]

So when action is executed, it'll just not work at all, because after the first branch finishes, the effect is no longer there.

Yes, this strategy just doesn’t work when computations can be reentrant (which capturing the continuation allows), which is why supporting all these things together is hard. eff uses a different, somewhat more elaborate strategy that effectively ensures handler state is associated with a particular continuation frame, even in the presence of delimited control.

[re-xyr]

But even if it didn't use bracket (like cleff afaik), it would use the same listen in both branches, so it wouldn't behave "nicely" anyway, i.e. it would have semantics of mtl + pipes.

Indeed - you would need to implement it according to eff (i.e. some kind of dynamic-wind), which properly restores state for each resumption call: https://github.com/lexi-lambda/eff/blob/master/eff/src/Control/Effect/Internal.hs#L797-L805

(I should say that I've been picking up all my effect system knowledge along the course of a few months - so if what I say now conflicts with what I said weeks ago, I apologize)