Supporting Basic Generics before Advanced Generics

[RossTate]

In yesterday's presentation, @rossberg recapped some of the advanced challenges to managing generics. While these advanced challenges are important, they are common to both structural and nominal types, and so I would like to first take a step back and call attention to some more basic challenges with generics that nominal types have already addressed but that structural types cannot overcome.

Consider the example of C# arrays that were prominently featured in the presentation. For 20 years, no one has been able to design a (decidable) structural type system that can express even just the low-level safety invariants of C# arrays. I warned of these issues when I first tried to get involved with WebAssembly, and more recently posted #138 to prompt broader group discussion of them, and there still seems to be no solution in sight even for easier cases like Java arrays. This means that C#, Java, Kotlin, and many other languages will have to compile their arrays (of reference types), regardless of the specific reference type, to just array anyref in the current structural Post-MVP and will always cast accessed values. Meanwhile, there is a 15-year-old paper showing how to express these arrays with nominal types, a 12-year-old paper actually putting nominal types into practice in an existing compiler for C#, and a 10-year-old paper showing how to make it practical to generate these types (plus an accompanying tech report providing the necessary theory for generalizing the approach to other classes of languages).

As for typed functional languages, consider the example of polymorphic recursion that was also prominently featured in the presentation. As pointed out in #119 (comment), the common application of polymorphic recursion discussed in the literature is handling expansive-recursive types, with the function collect for flattening a datatype 'a T = EMPTY | NODE of 'a * (('a T) T) into a list being the prominent used-in-industry ML example discussed. This type is inexpressible in the Post-MVP and in any decidable structural type system because expensive-recursive structural subtyping is known to be undecidable.¹ The lack of expressiveness means that the NODE wasm-structure will have to be a pair of 'a and T-of-anyref or the like, losing the invariant that this latter data structure is comprised of 'as. And, since ML types are erased, there is no way to dynamically cast these values to 'a, which means that collect cannot guarantee the resulting list is comprised of only 'as. If 'a were to denote string in some context, then this means that there is a string list that is not guaranteed (according to wasm's type system) to contain only string values, which consequently means wasm functions taking string list cannot demand the list only contains strings. So any compilation of ML programs with expansive-recursive types into the current Post-MVP will have to ignore type arguments on lists (and in fact all generic types) and just insert casts everywhere, just like C#/Java/Kotlin arrays have to. Meanwhile, nominal types are able to express this feature because they allow one to define an expansive structure without also making subtyping expansive (just like how the type 'a T in ML denotes an expansive structure but is not a subtype of anything).

So, in debating between structural and nominal types, before advancing into discussing the likes of how a nominal Post-MVP will represent the RTT for string[][][] (which the above three papers can all do) or a ((String T) T) T (which the techniques in the above tech report can do), we should first acknowledge that a (decidable) structural Post-MVP cannot even express the structural types of string[] or String T to begin with.

---

¹Right now we can decide subtyping between equirecursive types by viewing them as finite automata, with (unparameterized) fixpoint type variables serving as the back edges. Unfortunately, when the variables can be parameterized, that corresponds to generating a new set of automaton states rather than being able to cyclically reuse existing automaton states, meaning the automaton is no longer finite. One can also encode a Turing machine as an infinite automaton, incorporating the state of the string directly into the states of the automaton, and it turns out expansive-recursive types can express this encoding. See, for example, this encoding of Turing machines using expansive recursion in Java generics—an encoding can easily be translated to use structural types instead. This is not problematic for Java at the low level because Java erases its generics, but C# reifies generics and consequently disallows expansive inheritance to prevent this problem (due to this paper). And it is known that expansive nominal inheritance is not used in practice, even when permitted, though expansive structures are.

[conrad-watt]

For 20 years, no one has been able to design a (decidable) structural type system that can express even just the low-level safety invariants of C# arrays.

To be clear, this is about expressing covariant (source) arrays in terms of invariant (target) arrays? To play devil's advocate, what if WebAssembly were to be extended with a language-level covariant array that checks stores (e.g. by requiring an RTT argument)?

[rossberg]

Sigh. We really need to get away from all these false dichotomies.

• having structural types =/=> not having nominal types
• having structural types =/=> having equi-recursive structural types
• having only structural static types =/=> having only structural dynamic types
• having limitations in the MVP =/=> having the same limitations post-MVP

I have made these observations before. The second I actually wanted to talk about on Tuesday, but I didn't get to it.

And let me point out once more that any "nominal" semantics that we introduce must be "structuralised" at least at module boundaries, otherwise we would not be able to define linking. Once you accept that fact, it becomes obvious that nominal is only going to be a quasi notion and that much of this discussion is a red herring. For example, you can recast nominal recursive types as iso-recursive types in a structural manner. (OTOH, iso-recursive types are not enough for all languages either.)

[tlively]

And let me point out once more that any "nominal" semantics that we introduce must be "structuralised" at least at module boundaries, otherwise we would not be able to define linking.

I believe everyone is on the same page about this. Type imports must fully describe the structure of the type that is being imported no matter what system we use so that the compilation phase can determine field offsets. Whether equi-recursive, iso-recursive, or nominal, we all agree that WebAssembly's types should serve only to describe the low-level structure of data so that engines can emit safe and efficient code. Nominal types are being proposed not to get around this or to serve some other purpose, but merely to improve the algorithmic complexity of type canonicalization and various post-MVP extensions. In particular, nominal types are not meant to embed source-level type systems into WebAssembly, which we all agree is a non-goal and also generally impossible.

[RossTate]

To be clear, this is about expressing covariant (source) arrays in terms of invariant (target) arrays?

The problem with arrays arises more generally when the type system needs to simultaneously reason about subtype polymorphism and parametric polymorphism. For example, Kotlin arrays are invariant (putting aside dynamic concessions Kotlin makes on limited non-native platforms), but Kotlin also allows use-site (technically mixed-site) variance, which means one can have a (read-only) covariant Array<out Foo> type or a (write-only) contravariant Array<in Foo> type.

Expressing the low-level structure of these types requires bounded quantification. Unfortunately, because structural types identify structure and types, this means they need impredicative bounded quantification to express these examples, meaning that they quantify over structural types themselves. All the known subtyping rules for impredicative bounded quantification that can express the above subtypings are undecidable by some reduction to the result in this 1993 paper. Nominal types, on the other hand, make a distinction between structures and types (the latter is a layer of abstraction above the former), which means they can express these examples with predicative bounded quantification, quantifying over the layer of abstraction above structures rather than structures themselves. The tech report I mentioned above provides a framework for developing predicative quantifications that can decidably express a wide variety of languages.

[conrad-watt]

For example, Kotlin arrays are invariant (putting aside dynamic concessions Kotlin makes on limited non-native platforms)...

Expressing the low-level structure of these types requires bounded quantification.

I feel it's worth noting explicitly, as I discussed with @RossTate over email, that Kotlin's JVM backend implements (invariant) Kotlin arrays in terms of (covariant) JVM arrays. In this sense, the JVM backend does not succeed in "expressing the low-level structure" of the Kotlin array type, but nevertheless achieves performance which is far better than the array anyref approach.

I agree its preferable to allow as much expressiveness in Wasm as possible, and it may well be possible to make Wasm's type system expressive enough to handle this case fully faithfully, but the ability to "express the low-level structure" of a source-language type isn't a hard precondition for acceptable performance (and will not be possible in all cases).

[titzer]

Type imports must fully describe the structure of the type that is being imported no matter what system we use so that the compilation phase can determine field offsets.

Unfortunately Wasm-level linking is not enough to express the source information necessary to do proper late binding of source constructs (e.g. inheriting from a class across a module boundary). It is not possible for a source language like Java that wants to provide proper separate compilation to rely on Wasm type imports (even with full a structural description) for this. That problem is entirely orthogonal to the structural/nominal discussion.

[titzer]

Expressing the low-level structure of these types requires bounded quantification.

I don't understand why covariant read-only array views with dynamic RTT-based casts to writable array views doesn't work.

[conrad-watt]

I don't understand why covariant read-only array views with dynamic RTT-based casts to writable array views doesn't work.

My understanding is that this (or something like it) would specifically solve the performance concerns raised for Java and C# arrays, and Kotlin arrays up to the approach they use for the JVM backend (which introduces some minor gotchas).

If I'm understanding @RossTate's overarching proposal correctly, he knows of and has worked on a way of modelling covariant arrays with store checks, Kotlin arrays, C#'s reified generics, the this parameter of virtual functions (e.g. see here), and possibly expansive-recursive types (although I don't fully understand the example) using a single unified mechanism based on bounded quantification. This is described in the papers he's linked above (and elsewhere).

Clearly all else being equal it's preferable to have one generic [sic] mechanism for making all of these different source language features efficient rather than plug one specific (but very important) set of cases with a comparatively bespoke feature. I believe @rossberg would also agree. @RossTate's position is that a unifying approach based on bounded quantification will only be possible under a nominal type system, because a structural type system with sufficient expressivity for the examples above would be undecidable.

EDIT: it is worth noting that a Wasm-level covariant array would have the advantage that it could potentially be an MVP or soon-after-MVP feature.

[RossTate]

Classes and interfaces with (sound) generic methods also require bounded quantification to describe their structure, and you need to employ subtyping checks to ensure a class correctly implements its interfaces or extends its superclass. So again this is undecidable with structural types but decidable with nominal types.

It seems that the decidability limitations of structural types mean that no polymorphic language would be able to target a structural GC type system without erasing all polymorphism in their structures and just casting everywhere instead, like they would do if they were to target the JVM.

[aardappel]

@titzer

Unfortunately Wasm-level linking is not enough to express the source information necessary to do proper late binding of source constructs (e.g. inheriting from a class across a module boundary). It is not possible for a source language like Java that wants to provide proper separate compilation to rely on Wasm type imports (even with full a structural description) for this. That problem is entirely orthogonal to the structural/nominal discussion.

I feel this is what is essential to get some more agreement on, as a lot of design decisions hinge on how we view this. There's a lot of discussion that includes "but we must do it this way for languages to be able to do separate compilation" or "retain modularity".

But it seems that, while languages can choose to compile what they consider a "program" consisting of many language level modules to many Wasm modules, you can't often escape the need for the language to have additional information (outside Wasm) on how those modules fit together, and thus really must consider that group of modules as one unit, where representational choices of imports/exports internally to that "program" may change incompatibly when source level constructs change.

This informs our decisions of why GC types need uniform representation and/or subtyping etc, and to what extent implementations can specialize instead. @rossberg's argument of the existence of things like recursive polymorphic types entailing that we must therefore have these features may well change if we agree that modularity of a source language doesn't necessarily map to the same kind of modularity properties at the Wasm level.

[KronicDeth]

if we agree that modularity of a source language doesn't necessarily map to the same kind of modularity properties at the Wasm level.

Lumen using the GC proposal is still iffy (we have a GC in Rust that works and are probably more likely to want stack walking to rewrite roots), but if we are to use it, we have no plans to compile each Erlang module to a separate WASM module. That's actually counter to the reasons for Lumen: we want whole program optimization and so want a single file at the end. If we wanted multiple files we could have more closely matched how the BEAM VM works with .beam bytecode files.

[rossberg]

@aardappel:

There's a lot of discussion that includes "but we must do it this way for languages to be able to do separate compilation" or "retain modularity".

Yes, because it is a prominent use case. If you look at the landscape that exists already, then people do not actually want to build a new implementation of C# -- that would require duplicating a huge ecosystem effort. Instead, they want to implement .NET and reap the benefits of that. See Blazor. I suspect that similar considerations will hold for significant parts of the Java ecosystem. Non-modular approaches are a non-starter for that, because modularity is deeply engrained in these systems.

@tlively:

In particular, nominal types are not meant to embed source-level type systems into WebAssembly,

It's a bit more nuanced. In previous discussions, various people very much assumed and expected to be able to directly implement language-specific type tagging via Wasm-level runtime types. @RossTate in particular argued strongly for this being crucial in the case of OCaml's value representation. So I'm a bit fuzzy on what I am supposed to deduce from him making practically the opposite argument for a C#/.NET value representation now.

Nominal types are being proposed not to get around this or to serve some other purpose, but merely to improve the algorithmic complexity of type canonicalization and various post-MVP extensions.

One point I was trying to make in my presentation (but didn't quite get to) was that the algorithmic complexity argument is a red herring. As I showed, there has to be an implementation of dynamic structural canonicalisation somewhere. Whether that's in user code or the engine does not change its complexity. The only leeway with it really is the semantics of recursive types, which affects the complexity canonicalisation. But that question is entirely independent from the whole nominal distraction of an argument.

@titzer:

Unfortunately Wasm-level linking is not enough to express the source information necessary to do proper late binding of source constructs (e.g. inheriting from a class across a module boundary).

Not with what's in the MVP, no. But how do OO engines implement dynamic linking? By additional indirections, i.e., with offset tables. So what we should enable is expressing these techniques in Wasm, e.g., by introducing "member references" as a post-MVP feature. I have not heard an argument why this should not be possible.

@conrad-watt:

Clearly all else being equal it's preferable to have one generic [sic] mechanism for making all of these different source language features efficient rather than plug one specific (but very important) set of cases with a comparatively bespoke feature. I believe @rossberg would also agree.

I do, but obviously the price has to be adequate. If it amounts to putting complex and OO-specific custom typing machinery into Wasm then it's not clear if that's worth paying. Bounded existential quantification as a general mechanism is desirable, but already magnitudes more complicated than anything that the CG has been willing to put up with in the past. I think this will change, but not as fast and radically as some people hope. It would certainly turn Wasm into a very different language.

[tlively]

As I showed, there has to be an implementation of dynamic structural canonicalisation somewhere.

Apologies if I missed it in your presentation, but could you elaborate on why this is?

[titzer]

But how do OO engines implement dynamic linking? By additional indirections, i.e., with offset tables. So what we should enable is expressing these techniques in Wasm, e.g., by introducing "member references" as a post-MVP feature. I have not heard an argument why this should not be possible.

OO engines do not use additional indirections, offset tables, etc to implement late binding. Late binding requires source information and types and no amount of indirection is a substitute for logic that applies name matching and overloading rules. E.g. declarative linking rules will never be enough to express even Java's semantics here. It requires a runtime system and the preservation of source level types and names.

[tlively]

@titzer, what would you say the takeaway from that is for the current discussion? It seems to me that the complexities of late binding mean that it's not a problem we should be trying to solve in this MVP proposal, so we can mostly ignore it for now with the understanding that some future proposal will introduce a new staged or layered compilation/instantiation scheme to address it.