Operational semantics for throwing exceptions to other threads in Haskell

Question

I've read "Tackling the Awkward Squad" paper by SPJ and most of it was quite easy to follow however I didn't completely understand what exactly those two conditions above the separation line mean:

In paper it is stated that they are here to ensure that the second context (E2) is maximal, i.e. it includes all the active catches. However I do not completely understand what it means. Does it mean that an exception won't be thrown if there is a catch inside of a second thread? But why is bind also there then?

Answer 1

Intuitively, it is used to "insert" the exception ioError e in the right place, in a deterministic way.

Consider M = catch (threadDelay 1000000) someHandler. We have both:

M = Ea[M]
   where Ea[x] = x
M = Eb[M']
   where Eb[x] = catch x someHandler
         M' = threadDelay 1000000

without the side condition, we would have two distinct operational steps, making the semantics non-deterministic:

{throwTo t e}s | {M}t ==> {return ()}s | {Ea[ioError e]}t
                        = {return ()}s | {ioError e}t
{throwTo t e}s | {M}t ==> {return ()}s | {Eb[ioError e]}t
                        = {return ()}s | {catch (ioError e) someHandler}t

In the former case, the error is not caught, in the latter it is. The side condition ensures only the latter is a valid step.

Bind is there as well to avoid replacing everything in:

M = catch (threadDelay 1000000) someHandler >>= something

Here, if you only require "M not a catch", you could again choose M = Ea[M] and replace all the code. The side condition instead forces you to choose

Ec[x] = catch x someHandler >>= something

and insert the ioError e in the correct place inside the catch.