Best way to implement "scoped exceptions"?
I'd like to implement "scoped exceptions"[1], that is, a combinator of type withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) so I can use exceptions in a convenient way, without having to set up fragile "action at a distance" based on the type of the thing I'm throwing and catching, for example: scopedExceptionExample :: IO (Either String (Either Int Void)) scopedExceptionExample = do withScopedException $ \throw1 -> withScopedException $ \throw2 -> if (1 :: Int) < 0 then throw1 "Hello" else throw2 1234 -- ghci> scopedExceptionExample -- Right (Left 1234) Here's a hacky way of doing it, based on tagging each exception with a unique value, and then filtering when handling: data MyException where MyException :: e -> Data.Unique.Unique -> MyException instance Show MyException where show _ = "<MyException>" instance Exception MyException withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) wiathScopedException f = do fresh <- Data.Unique.newUnique flip tryJust (f (\e -> throwIO (MyException e fresh))) $ \case MyException e tag -> -- unsafeCoerce is very unpleasant if tag == fresh then Just (unsafeCoerce e) else Nothing This is the approach taken by the effectful library[2]. But is there a better way? Can I persuade GHC's RTS to work like this directly? Tom [1] I don't know if these already have a name [2] https://hackage.haskell.org/package/effectful-core-2.2.1.0/docs/src/Effectfu...
Sounds to me a bit like CPS - so maybe something like callCC: https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-...
On Wed, Dec 28, 2022 at 09:19:20PM +0000, Dan Dart wrote:
Sounds to me a bit like CPS - so maybe something like callCC: https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-...
Thanks. There is some element of CPS to it, although in this case I'm specifically looking for an API that's plugged in to how GHC's RTS treats exceptions.
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... On 2022-12-29 1:02 PM, Tom Ellis wrote:
Sounds to me a bit like CPS - so maybe something like callCC: https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-... Thanks. There is some element of CPS to it, although in this case I'm specifically looking for an API that's plugged in to how GHC's RTS
On Wed, Dec 28, 2022 at 09:19:20PM +0000, Dan Dart wrote: treats exceptions. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
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. Thanks Li-yao! Tom [1] https://gist.github.com/sebfisch/2235780
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
On Wed, Dec 28, 2022 at 08:38:04PM +0000, Tom Ellis wrote:
I'd like to implement "scoped exceptions"[1], that is, a combinator of type
withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) [...] Here's a hacky way of doing it, based on tagging each exception with a unique value, and then filtering when handling:
data MyException where MyException :: e -> Data.Unique.Unique -> MyException
instance Show MyException where show _ = "<MyException>"
instance Exception MyException
withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) wiathScopedException f = do fresh <- Data.Unique.newUnique flip tryJust (f (\e -> throwIO (MyException e fresh))) $ \case MyException e tag -> -- unsafeCoerce is very unpleasant if tag == fresh then Just (unsafeCoerce e) else Nothing
This is the approach taken by the effectful library[2]. But is there a better way? Can I persuade GHC's RTS to work like this directly?
I found a better way, or more accurately LSLeary suggested it to me, now implemented in Bluefin.Internal.Exception.Scoped: https://hackage-content.haskell.org/package/bluefin-internal-0.1.0.0/docs/Bl... The innovation is to have a `Key` type that supports: newKey :: IO (Key a) eqKey :: forall a b. Key a -> Key b -> Maybe (a :~~: b) This allows us to tag thrown values with a `Key` and unwrap them only when we have another copy of the same key, which allows us to obtain type equality. (`Key` is also available in Apfelmus's `vault` package.) Tom
I think "scoped exceptions" is basically also the same thing as what https://github.com/tek/polysemy-resume#readme implements, so it might be of interest to you. On 5/25/25 19:32, Tom Ellis wrote:
On Wed, Dec 28, 2022 at 08:38:04PM +0000, Tom Ellis wrote:
I'd like to implement "scoped exceptions"[1], that is, a combinator of type
withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) [...] Here's a hacky way of doing it, based on tagging each exception with a unique value, and then filtering when handling:
data MyException where MyException :: e -> Data.Unique.Unique -> MyException
instance Show MyException where show _ = "<MyException>"
instance Exception MyException
withScopedException :: ((forall a. e -> IO a) -> IO r) -> IO (Either e r) wiathScopedException f = do fresh <- Data.Unique.newUnique flip tryJust (f (\e -> throwIO (MyException e fresh))) $ \case MyException e tag -> -- unsafeCoerce is very unpleasant if tag == fresh then Just (unsafeCoerce e) else Nothing
This is the approach taken by the effectful library[2]. But is there a better way? Can I persuade GHC's RTS to work like this directly? I found a better way, or more accurately LSLeary suggested it to me, now implemented in Bluefin.Internal.Exception.Scoped:
https://hackage-content.haskell.org/package/bluefin-internal-0.1.0.0/docs/Bl...
The innovation is to have a `Key` type that supports:
newKey :: IO (Key a) eqKey :: forall a b. Key a -> Key b -> Maybe (a :~~: b)
This allows us to tag thrown values with a `Key` and unwrap them only when we have another copy of the same key, which allows us to obtain type equality. (`Key` is also available in Apfelmus's `vault` package.)
Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (5)
-
Dan Dart -
Georgi Lyubenov -
Li-yao Xia -
Tom Ellis -
Tom Ellis