mitchellwrosen/safe-exceptions-checked

What is story for `catches`

3noch opened this issue · 3 comments

3noch commented

The base docs for catches says that it resolves two issues caused by nesting exception handlers. However, this library does not provide catches (the type would be pretty tricky). What is the recommendation when trying to handle multiple exception types in the same handler? It should be at least documented.

Interesting question! I'm not sure. Note that in a world where all exceptions are checked, the concern that one handler might catch another's exception can be mitigated by reordering them (at least in some cases).

For example, say we have

x :: (Throws Foo, Throws Bar) => IO ()
f :: Throws Bar => Foo -> IO ()
g :: Bar -> IO ()

If we write

x `catch` f `catch` g

then g will discharge the Throws Bar constraint induced by x and f, catching Bar exceptions thrown by either in the process.

But if instead we write

x `catch` g `catch` f

then we're happily left with a Throws Bar constraint due to f, which we purposely did not want to handle with g.

By the way, I've personally never used this library, as the idea seems fundamentally flawed in many ways that were not evident to me after reading the Well Typed blog post. For example, consider forkIOing a Throwing computation.

bomb :: Throws Bomb => IO ()
forkIO bomb :: Throws Bomb => IO ThreadId

Oops, the calling thread got stuck with having to discharge the constraint, which is clearly wrong (though the uncheck escape hatch can save us here). Furthermore, we're not forced to handle the possibility that the forked thread throws an exception, which would simply call the uncaught exception handler and print to the console (if not overridden). It seems like checked exception machinery should force you to handle this case.

I'm eager to hear if you are having any success with this library, as the concept is, in theory, very valuable. But at the moment I've just been embracing the unchecked, extensible exception hierarchy, and at times wishing there was a decent alternative design (or at least that there was more of a cultural emphasis on extensively documenting exactly what the exception hierarchy that ships with your library is, ascii-tree diagrams and all, plus exactly which functions might throw what).

Cheers!

3noch commented

Thanks for the clarifying thoughts! I hadn't considered the forkIO situation. At least for this particular example, the solution seems simple (but not very satisfying): Make a different forkIO for that moves the constraint into the thread somehow (e.g. forkIO :: (Throws e => IO ()) -> (Throws e => IO ()) but I'm not sure that's valid Haskell...). Alternatively, since these only work with synchronous exceptions, forking probably shouldn't even be possible in the presence of unhandled exceptions, unless the parent and child thread are linked. So I could imagine the problematic type being correct in the presence of linking.

Re: success. I'm not actually using this library either. I attempted a simple experiment and immediately ran into the need for catches but found there was no such combinator here. It's somewhat understandable as the type would be very complex. I also find it surprising that the Throw constraint is not multiparameter. It seems that Throws m e would be a more obvious type and I'm not sure why the Throw is not attached to a particular monad. This would also "solve" the forkIO problem because it wouldn't work on naked IO.

@3noch I'd propose that one way to circumvent the necessity of catches is, if you have the liberty, to define a new datatype that wraps all of the exception types that you're interested in catching; e.g. if you want to catch exceptions of type A, B, and C, you can define a new ADT data AppException = AppExceptionA A | AppExceptionB B | AppExceptionC C and then just use catch, pattern matching on the constructors instead of using the list of existentially quantified handlers to account for the different exception types

It seems to me like you might be able to accomplish catches with some type level list of exceptions; e.g. instead of the constraint (Throws e1, Throws e2, ..., Throws eN) => you could have something like a type level list (All Exception xs, ThrowsList (xs :: '[*])) => and a heterogenous list of handlers that return a computation with the type level list of exception types that weren't caught by the list of handlers. I played around with trying to write such a function here in this comment, but it's clear I need the GHC typechecker's aid to produce anything at all of value.

@mitchellwrosen regarding the forkIO issue... yeah, maybe this approach doesn't work for multi threaded code... I can't easily imagine how to force the constraint on the body of the forkIO code and not the calling thread 🤔