Open arybczak opened 2 years ago
(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.
(I assume you mean
speff-same-scope
; the other two branchesspeff
andspeff-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:
In other languages they are usually treated as very low level primitives and used as implementation detail for other control mechanisms.
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.
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
esSend
computation in a handlercontrol
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.
@arybczak Note that IO-native prompt
and control
doesn't "just work" in all scenarios; particularly, they won't be able to penetrate forkIO
s - 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.
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.
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.
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 throw
s. 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 control
s and only allow the resumptions to be called locally, then maybe there won't be this problem? ...
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.
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.
Please read the documentation for those primops before using them—using them with arbitrary IO
code is not safe.
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
I believe
bracket
is well-behaved wrtcontrol0#
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.
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.
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:
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.
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)
Can it be written? :thinking: