Nominal types vs. inter-module interaction

[jakobkummerow]

If I understand correctly, one of the biggest arguments for the current MVP's structural static type system is that it makes sharing types across module boundaries quite straightforward:

;; Module A
(type $string (array i8))
(function $hash (export "hash") (param (ref $string)) (result (ref $string))
 body...)
 
;; Module B
(type $my_string (array i8))
(function $hash (import "module" "hash") (param (ref $my_string)) (result (ref $my_string)))

...and things just work, because $string and $my_string are automatically recognized as being the same type.

Notable observations here are:

• "things just work" might be a bit of an exaggeration: the two modules must still intentionally choose to use compatible/identical type definitions. Maybe one of them publishes an API spec that the other adopts, or maybe both authors communicate out-of-band and discuss what types to use, etc.
• the names don't need to match, as the coordinating host (in case of browsers: JavaScript) can take e.g. one module's "md5hash" export and feed it to the other module's "stringhash" import.
• considering that Wasm modules are typically not handwritten but rather generated by toolchains, it is not entirely clear how developers writing "surface language" code (Java etc.) can even control/influence the Wasm types that their toolchain will generate for them. Maybe this whole multi-module scenario is only realistic for sets of modules produced in one go by the same version of the same toolchain having a whole-program view of the surface language source? If so, that would likely change our collective perspective on a bunch of the concerns discussed below.

Now, if we switched the static type system to nominal semantics, that would in particular mean that two type definitions give us two distinct types, so the example above would no longer work "just like that". To still support cross-module object sharing, e.g. for function calls, we have to find an alternative solution.

One idea is to not change what happens at the module boundary, i.e. keep structural typing there. In a case like the above, where a module attempts to satisfy a function import with another module's function export and these functions use certain types, the engine would automatically try to match the types. I believe that this would work for the module interaction case, however it creates another problem: merging modules would potentially change semantics, and that is unacceptable. (Merging two modules is straightforward and should work fine, but consider a three-module case: module M imports functions from N and O, the modules define types $m, $n, $o that are structurally identical and used in these functions' signatures. If N and O are merged, the merging tool cannot know that $n and $o are supposed to be the same nominal type (because there are no function calls between N and O that would implicitly provide this information); when linking M with the merged NO, it becomes apparent that two nominally distinct types $n and $o in NO are supposed to match the same type $m in M. This would re-introduce structural type equivalence into NO "through the back door".) So I think this idea does not hold up to critical inspection.

Another idea that has been mentioned before is to import and export types just like functions:

;; Module A
(type $string (export "string") (array i8))

;; Module B
(type $my_string (import "module" "string") (array i8))

(Note that module B repeats the (array i8) type definition in order to allow separate compilation, i.e. we want to enable engines to compile code for B before having seen A or knowing that B will import things from A.)
That solves the problem of needing a single type, but creates a (potential?) new problem: it requires the modules to agree on the export/import role assignment. For functions, this is natural, because the whole point is that the function definition is large and complex and one module's responsibility. For types, this is less natural, especially if we imagine an NPM-style decentralized ecosystem of libraries: what if I want to import one module's string hashing function and another module's string compression function, who gets to export the string type used for these interactions?

Per the observations above, there is some doubt whether this scenario is realistic (and hence whether the concern is warranted), but we may want to avoid the issue anyway, so as not to paint ourselves into a corner. We could work around this difficulty by searching for more symmetric/flexible approaches to sharing types across different modules.

One idea is to define a symmetric version of the directed export→import concept. Maybe:

;; Module A
(type $string (importexport "string") (array i8))

;; Module B
(type $my_string (importexport "string") (array i8))

(Side note: maybe we should pick a different strawperson keyword than importexport, such as publicname, just to make (spoken) conversations less ambiguous: "importexport" sounds like "import/export", but describes a significantly different notion.)

Problems solved with this approach:

• we now have an explicit way to achieve the identification of two type definitions with one another that structural static types gave us implicitly. Notably, when two modules annotate two types this way as supposedly identical, the engine has to do the same structural type check as it does with the current MVP to verify this annotation's validity. (Or at least a very similar check; nominal types make recursive steps return more quickly but otherwise the algorithm is about the same.)
• there's no longer a need to select an exporting module, all modules have equal "rank" wrt. type definitions
• module merging is easy, as a merging tool knows exactly which types should be identified. (Such a tool may or may not perform its own checks to ensure that this identification of types is valid; if it is invalid, then the resulting merged module will be invalid and will fail validation later on.)

Problems created:

• the modules must agree on the name "string". I would argue that this is not a problem in practice: since even in the structural world, module authors have to agree on matching type definitions, they now simply have to agree on one more detail, which is the type's importexport name. That's not a significant increase in coordination burden.
• by having an implicit global shared namespace for importexport type names, there could be unintentional collisions. That is a serious concern that needs a solution.

Solution A: treat identical importexport names as requests that may well fail: a matching name causes the engine to perform a structural type check; if that check fails, then that's not a validation error, the types simply won't be identified with each other. If the two modules don't try to use the types in question for any interactions, then that's just fine. One way to look at this would be to say "we still have structural typing across module boundaries, but with the twist that the importexport name is part of the structural definition".

Solution B: analogous to how the coordinating host can map function exports to imports with different names, we could also empower (or burden) this coordinator with matching up type names. This would, effectively, give each module its own namespace for public type names. (This might be desirable in addition to solution A in order to solve the opposite problem: unintentional mismatches of type names.)

Solution C: please contribute other ideas by commenting :-)

Speaking of comments, I'm mostly trying to get a conversation / thought process started here. There may well be other problems that I have overlooked; please point them out! There may well be better, or at least additional, ideas for solutions that I haven't thought of; please present them!
If we're generally happy with nominal typing inside a module, it would be great to find a way to make it viable for multi-module scenarios as well -- maybe we can then finally arrive at a type system that we can reach consensus on?

To give credit where it's due: thanks to @tebbi, @rossberg, and @RossTate for having discussed these ideas with me. This post is more thought-through than it would have been without their input :-)

[dcodeIO]

Recently thought about something potentially related but in context of interface types: What if one module's string is (struct (field (i32 (ref array i16)))) and another module's string is (struct (field (i32 (ref array i16)))) as well, both using the name jstring by coincidence, but even though structurally identical, the i32 is a hashCode that is computed differently in what seems to be compatible? Will then fail late and apparently randomly at runtime, likely hard to debug. May well be that this is a non-concern in this context, but thought I mention.

[taralx]

I'm just going to say that, at first glance, this looks like the same problem that linkers try to solve using weak symbols.

[aardappel]

Solution A) is nice because it just improves upon structural typing with "nominal typing light", i.e. just reduce the amount of structural typing matches by additionally matching on tag "string". Unintentional collisions are thus not a serious problem, since they just make things strictly better than not having this tag at all.

And it's not hard to come up with more elaborate names that will not clash unless someone specifically wants to.

Conversely, you could allow people to still opt in to structural typing, by specifying "" as a name (matches structurally unless a tag is specified) or "*" (matches anything structurally). Again, that would make it strictly better than only structural typing.

[littledan]

Based on @rossberg 's observation that, to express generics, rtts might be dynamically created at runtime in a potentially unbounded way: this sort of canonicalization system would also have to be available at runtime. Maybe there could be an instruction that accepts an rtt and a some kind of chunk of memory, to cache the rtt in the system using the memory chunk as a dynamic key. (Or, it could be done in a user module which everyone is expected to import, as many others have discussed...)

[RossTate]

Based on @rossberg 's observation that, to express generics, rtts might be dynamically created at runtime in a potentially unbounded way.

This observation is false. There already exists a C# compiler that produces independently verifiable (i.e. typed) x86 that counters this claim.

[conrad-watt]

This observation is false. There already exists a C# compiler that produces independently verifiable (i.e. typed) x86 that counters this claim.

Could you make an issue that describes how this is done, with reference to the example @rossberg used in his slides?

[rossberg]

Based on @rossberg 's observation that, to express generics, rtts might be dynamically created at runtime in a potentially unbounded way.

This observation is false. There already exists a C# compiler that produces independently verifiable (i.e. typed) x86 that counters this claim.

My precise observations were:

1. The C#/.NET semantics allows for an unbounded number of dynamic type instantiations.
2. All these must be distinguishable at runtime by language-level (explicit and implicit) casts.
3. Hence an implementation of C#/.NET has to implement dynamic type generation.
4. If it ought to be able to piggyback Wasm RTTs and casts for that, then Wasm RTTs must be generated dynamically.

Please explain which of these is false. AFAICT, the only solution was to essentially forego the premise of (4) and implement a mirror RTT representation in user space. I believe that's what you said as well.

The problem with such an implementation is that it fundamentally requires "erasure" for generic type parameters. Hence it would not be able to benefit from more precise typing via Wasm-level generics once we add them, and would instead be left with "unnecessary casts" for each access to something typed by a parameter -- the very problem you complain about elsewhere wrt array accesses.

[jakobkummerow]

I think "the premise of (4)" is the crucial point. Yesterday's presentation sounded (to me) as if it took that premise as a given -- which I had trouble wrapping my head around, but clarifying that it is a conditional premise clears that up.

I think this premise is very much up for discussion. As even yesterday's presentation pointed out early on, the primary purpose of the types in WasmGC is to aid the engine in producing safe and fast code. Supporting every single feature of every single surface-level language's type system is a non-goal in particular because it is impossible.

For a low-level language with "assembly" in its name, it is appropriate and also nicely general/flexible to provide low-level primitives; we'd then expect module producers to build their individual required semantics on top of that. On the other hand, for better performance, we want to allow engines to (safely!) drop "unnecessary casts", which requires the type system to express somewhat higher-level (i.e. closer to the surface language) notions and guarantees. Clearly we have to draw the line somewhere.

I'm not sure where exactly we should draw the line; most folks on this issue tracker would probably agree that that's a very difficult question. I think it's fair to argue that supporting cast-free array element loads is more important than enabling dynamically generated type parameters to piggyback on the Wasm-level casts -- so drawing the line somewhere between these two wouldn't generally sound unreasonable to me. I mean, even if the C# type system allows you to generate String[][][][][] dynamically at runtime, (1) how often do you write such code, and (2) how often is it critical for the success of your app that such code can eliminate "unnecessary" casts?

[RossTate]

The problem with such an implementation is that it fundamentally requires "erasure" for generic type parameters.

Following up on @jakobkummerow's comment, this sentence seems to be the source of misunderstanding. On slide 36 of my presentation overviewing the related literature titled "Custom Casting with Identifiers", I showed how "nominal" typed assembly languages reason about casts at the assembly level. That is, these "nominal" systems are able to reason about casts below the level WebAssembly rtts; they can describe the invariant maintained by a WebAssembly engine's use of an array of identifiers in an object's GC descriptor and guarantee that the assembly instructions used to access that array and compare its content with a given rtt actually ensure the object has the type specified by the rtt. To these "nominal" systems, this data structure used by engines to implement rtts is just one of the many data structures that one can use to implement casting and that these systems can reason effectively about. Some of these data structures place the relevant casting information in the object's GC descriptor, while others (like that on slide 36) place these data structures in the object itself, which enables even a program with generics to be implemented with a finite number of GC descriptors (if it wants).

[rossberg]

@jakobkummerow, I agree, and that was kind of what I was getting at. Unfortunately, though, it does not matter how often such a features is used. In a separate compilation scenario you cannot make useful assumptions about that and usually need to compile for the general case. (The only localised scenario would be such a constrained and rare case that it’s hardly worth optimising for.) In practice, the implication is that you won’t be able to piggyback C#/.NET casts on Wasm casts.

That in turn means that adding generative RTTs to Wasm really only helps Java. Which raises the question that I have raised before: whether it is worth adding them at all for the MVP.

[rossberg]

@RossTate, yes, but that is assuming a whole machinery of highly non-standard and specialised typing extensions that I estimate would be post-post-mvp at best.

[RossTate]

Can you explain what you mean by "highly non-standard"? There is only one implemented system that is comparable to the Post-MVP goals of the GC proposal, and it uses these techniques, so I don't understand how you can classify them as highly non-standard.

[tlively]

I would like to voice my support for the importexport solution suggested here. In particular, I like that it solves the import/export asymmetry problem while keeping the benefits of nominal types. In particular, Wasm consumers would not need to do any graph canonicalization and calculating LUBs would be much simpler and faster, which is important for Binaryen.