On Thu, Dec 29, 2022 at 03:41:22PM +0000, Tom Ellis wrote:
On Thu, Dec 29, 2022 at 01:31:47PM +0000, Li-yao Xia wrote:
The recently implemented Delimited Continuation Primops proposal[1] features tagged prompts. That seems like just what you are looking for.
[1]: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0313-de...
Very interesting, thanks! My initial attempt at implementing scoped exceptions using the delimited continuation primops was bad:
withScopedExceptionBad :: ((e -> IO (Either e r)) -> IO r) -> IO (Either e r) withScopedExceptionBad body = do promptTag <- newPromptTag prompt promptTag $ do l <- control0 promptTag $ \myThrow -> do r <- body (myThrow . pure) pure (Right r) pure (Left l)
It was very head-scratching trying to work out how it should be implemented. Then with the help of a gist by sebfisch[1] I managed it:
withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) withScopedException body = do promptTag <- newPromptTag prompt promptTag $ do r <- body (\e -> control0 promptTag (\_ -> pure (Left e))) pure (Right r)
Surprisingly to me, for scoped exceptions, the handler passed to control0 should *ignore* its argument. That's because its argument allows it to escape from the call to control0, but we want to escape from the call to prompt. This is very powerful and mind-bending stuff and allows me to do exactly what I wanted.
Inspired by Alexis King's excellent talk recently at ZuriHac I reimplemented this in a more general way. https://www.youtube.com/watch?v=aaApZhfisbs ZuriHac 2023 — Alexis King — Delimited Continuations, Demystified "withScopedEffect" allows to use any handler you like for the "effect". withScopedEffect :: (a -> (IO b -> IO r) -> IO r) -> ((a -> IO b) -> IO r) -> IO r withScopedEffect handler body = do promptTag <- newPromptTag prompt promptTag (body (\e -> control0 promptTag (\k -> handler e (prompt promptTag . k)))) withScopedException :: ((e -> IO Void) -> IO r) -> IO (Either e r) withScopedException body = withScopedEffect (\e _ -> pure (Left e)) (fmap Right . body) Tom