should the proposal include type exports?

[lukewagner]

Thinking a bit more about type imports after #3, type exports actually raise some pretty important questions that, iiuc, we could otherwise punt on if all we really need in the short term (at least for getting statically-typed calls to host APIs) is type imports.

In particular, with type exports there are some interesting questions about:

• type equality (in wasm) and identity (in the JS API) and whether types are generative/applicative
• if i export a typedef (say, for now, a function type), can that type always be imported with the same structural type (as a (sub ...) bounds) or is it possible for me to export a type that is fully abstract (such that no other module can give it a type more specific than any)

Both relate to how type exports can be used to implement abstract data types, which I think is important, but technically not a problem we have to solve right now in this proposal, at least as currently motivated.

[rossberg]

Interesting point. Not sure it would be great to split this up further, since it'd be oddly asymmetric to have imports but no exports.

Either way, I think that type generativity should not be coupled to exports, since that makes for a rather complex semantics -- you'd get into many of the technical complications of the "sealing" construct for ML modules. Instead, it would be both simpler and probably more usable to make it a future feature of type definitions themselves.

Similarly, I think that the natural semantics for type exports is to be fully transparent. If we wanted to introduce some form of abstract export we can always add that later. But I suspect this is more or less the same problem as the first one, with the same answer, too.

[lukewagner]

Thanks, good points. If I could dig in a bit:

Agreed that generativity belongs on the type definition. So then, considering #3, does that mean that <consttype>s would similarly grow a way to specify generativity for i31 et al?

Abstract exports is more of what I'd like to understand. It seems like we'd need an export statement of the form "export A:<consttype> as B:<consttype>" (where A <: B). Is that how you were thinking it work, or is there another way to skin this?

Concretely, I'd like to understand how the answers to these questions come together to allow a module a.wasm to export an abstract type T, as well as operations on T, representing ref T with an i31ref, while ensuring only a.wasm could create or view ref T values via i31ref. (And similarly for anyref and funcref instead of i31ref.) This seems like the most valuable use of type exports I can think of, pre-wasm-GC.

[rossberg]

Good question. A common way to support abstract data types in user-facing languages is having some form of explicit injection/projection operators that can be hidden independently from the type itself. For example, in Haskell you have the newtype declaration:

newtype Time = Secs Int

This defines the type Time and the constructor Secs. The representation of type Time is exactly the same as Int, but you have to apply the Secs constructor to inject an Int value into it (and pattern-match the constructor to project). Operationally, these are no-ops however, so the constructor can be seen as a type converter. Notably, a Haskell module can export Time without exporting Secs, thereby achieving abstraction.

I'm not entirely sure yet what the best way would be to port such a mechanism to Wasm, but it should be doable somehow. FWIW, the exception proposal already introduces a notion of constructor that enables the same kind of abstraction, though it is designed for a different use case and isn't a no-op. (But the exception example also shows that abstraction/encapsulation does not necessarily require introducing generative types if you already have generative values. But they seem necessary if you want to make abstraction a no-op.)

[lukewagner]

Ah hah, so, iiuc, the newtype route would mean that if we had a consttype A which we wanted to export abstractly, we'd create some newtype type definition B (in the type section), and we'd export B? That does seem simpler than trying to talk about different views of the same typedef (as in the approach I was imagining, which I think is analogous to the ML sealing approach).

So then, iiuc, with the current proposal in this repo, all types are non-generative and non-abstract, with generativity/abstract types addable in the future by adding new kinds of type definitions?

[rossberg]

Yes, yes, and yes. :)

[lukewagner]

Ok, cool, thanks for the discussion!