I noticed that the GC proposal overview says a lot about typing, tagging, subtypes, mutability, type-equivalence, and methods.
Excerpts:
- In order to avoid spurious type incompatibilities at module boundaries, all types are structural. Aggregate types are considered equivalent when the unfoldings of their definitions are...This is the standard definition of recursive structural equivalence for "equi-recursive" types
...
- Want to represent objects as structures, whose first field is the method table
While the actual spec draft doesn't say anything about methods or tagging, it seems like these concepts are very important to the design.
Why? Especially: why does the design have sophisticated opinions about type equality?
Owner of the GC Proposal here.
I am not entirely sure what precisely you are asking. Wasm is typed, so clearly, the proposal needs to define what types are equal or when a type is a subtype of another. That determines what programs validate and which don't. The rules need to be type-sound in order to prevent safety breaches without requiring runtime checks. For type equivalence we just suggest the canonical, most permissive semantics possible, similarly for subtyping. Furthermore, to get useful subtyping in practice, a producer needs to be able to restrict where mutation is allowed, because e.g. mutable fields cannot soundly allow subtyping.
It turns out that an adequate design and formulation of the typing rules around general GCed data types is actually far more intricate than defining their operational behaviour -- that is fairly simple, and does what you would probably expect.
The GC extension does not include anything like methods or method tables as primitive features. However, it is an important design goal that such notions are expressible with what the proposal provides, since we want to support the compilation of languages that have such concepts.