Semantics for duplicated resume table entries

[dhil]

The instructions resume and resume_throw are annotated with dispatch tables, which consist of a collection of (on $tag $label) or (on $tag switch) associations. There is no restriction on how many times a particular $tag is allowed to appear the dispatch table, e.g. the following is currently valid:

(resume $ct (on $tag $label1) (on $tag $label2))

The question is what is supposed to happen when the child computation performs (suspend $tag)? I imagine the answer might be "whatever exception handlers do" (the first entry shadows the second entry). However, with the recent extension of switch we have an additional case to consider as the following is currently valid (syntax) too:

(resume $ct (on $tag $label) (on $tag switch))

But what does it mean? In principle we can view $tag as naming two separate control effects, which we differentiate at runtime by how $tag is invoked, i.e. either using suspend or switch. So an argument can be made for allowing $tag to be both "suspendable" and "switchable". Though, if we choose this semantics, then it imposes an odd restriction on the type of "suspendable" $tag as for it to be switchable it must have type $tag : [] -> [t*].

[conrad-watt]

Based on the semantics @tlively discussed previously, I think we treat the signals from suspend and switch as totally separate, so each suspend matches the first on... $label handler with the right tag, and each switch matches the first on ... switch handler with the right tag. Handlers of the "wrong" kind are just totally ignored.

[dhil]

Based on the semantics @tlively discussed previously, I think we treat the signals from suspend and switch as totally separate, so each suspend matches the first on... $label handler with the right tag, and each switch matches the first on ... switch handler with the right tag. Handlers of the "wrong" kind are just totally ignored.

I am understanding you as (resume $ct (on $tag $label) (on $tag switch)) is well-defined in the sense that suspend $tag jumps to $label, whilst switch $tag direct switches to the given continuation argument.

[conrad-watt]

That's my current understanding, yes! @tlively can catch me if I'm misrepresenting.

[tlively]

Yes, @conrad-watt is correctly representing what we had discussed before. There’s a paragraph in the explainer informally laying this out.

[dhil]

Patch #82 implements the semantics discussed here. I am happy to close this issue for now.