Could the proposal expand/clarify the notion of exception tag identity?

[lukewagner]

Right now the concept of exception tag when introduced is a bit fuzzy: the first use says "Within the module, exceptions are identified by an index into the exception index space. This index is referred to as the exception tag."

I think tags need to be introduced first by saying that they are runtime objects that have (1) a unique identity (2) a type signature and that exceptions are "branded" with a tag on creation and catch blocks match exceptions by specifying a tag's identity to match. This is all independent of index; indices are just the way that throw/catch within a module refer to a defined/imported tag identity. It'd also be good to call out the symmetry to memory/table definitions and that sharing or the lack thereof between instances in a single app is controlled by the user by which identities are used to instantiate.

Lastly, while the core wasm spec doesn't say how a host environment can create multiple instances, it should speak to multiple instances being able to import the same exception tag identity and therefore throw and catch each others exceptions and this would be the basis for, e.g., C++ dynamic linking.

[rossberg]

One additional observation: in languages with similar exception mechanisms (e.g. ML) it has repeatedly been discovered that tags are a useful construct for a variety of things other than exceptions. Yet programmers shy away from using them for those other purposes because it looks misleading/abusive to define, say, a message token as an "exception".

In the light of this, I would suggest to simply call these "tags", "tag type", "tag section" etc. With the current proposal, forming exceptions would be the only use of tags, but for example, allowing tagged values in tables would open up a different set of use cases for them.

[KarlSchimpf]

My understanding is that the "exception tag", like a function index, is there to allow the code to refer to which type of exception is being thrown. Each entry in the exception section, and each corresponding imported entry refer to an (opaque) exception type. There can be multiple instances of each exception type. It is also the responsibility of a dynamic linker to provide a mechanism to unify exception tags and types of exceptions.

[rossberg]

Not quite. The terminology that would best match the underlying semantics as well as existing notions in Wasm would be the following:

• tag: an opaque dynamic token with identity that can be used to form tagged values.
• tagged value: a tuple created from a tag and suitable attribute values.
• tag type: the signature of a tag describing the attributes associated with it in a tagged value.
• tag import: an entry in the import section that specifies an unknown tag with a tag type.
• tag definition: an entry in the tag section that defines a new tag with a given tag type.
• tag index: a static index that references a tag in the import or tag section of a module.
• exception: a tagged value created for the purpose of exception handling.

So, tag ~ function, tag index ~ function index, tag type ~ function type. In particular, a tag is not itself a type, it has a type. It is not an index either, it is referenced by an index (inside a module). Tags are dynamic entities with global meaning (created either by instantiating a module with tag definitions or by API methods), while indices only have a relative meaning inside a given module.

[eholk]

@rossberg-chromium, is your proposal similar to adding sum and product types, or open unions? I'm guessing it's not quite the same, because ML has sum and product types and programmers definitely do not shy away from using them. What are the differences?

[rossberg]

@eholk, the exception mechanism in this entire proposal is pretty much identical to ML-style exceptions, whose values in literature are called extensible sums, among other things. They aren't ordinary sum types, since they are infinite and can be extended dynamically. "Open union" sounds reasonable, though I'm not sure it has an unambiguous meaning.

[eholk]

@rossberg-chromium, thanks. "Extensible sums" sound like what I am thinking of for "open unions." I think the open union term comes from Typed Racket or a related community.

[aheejin]

I think we can close this now.