Instantiating abstract types

[awendland]

I was wondering if further discussion had occurred on how abstract types would be instantiated. I was chatting with @lukewagner, and he mentioned that the Haskell-esque newtype approach mentioned by @rossberg in #4 (comment) was his understanding of the latest direction, but specifics on how a concrete value was converted into the abstract type were still undefined.

---

One approach (similar to Ocaml's abstract types) could be to have a typedef that acted as an alias when used inside the module and as a distinct nominal type when used outside:

(module
  (newtype $T i32)
  (func $createT (param i32) (result (ref.type $T))
    (local.get 0))
  (export "T" (ref.type $T))
)

Internally, this module could have an identity function for construction such as $createT. However, outside of this module, this function wouldn't type check because an i32 != T (only inside the module does this equivalency hold).

[rossberg]

Yes, abstract types (which haven't originally been a priority) still need some design. I agree that something between Haskell's newtype and ML-style module sealing semantics is probably where we will land, and your example is roughly the kind of thing I have in mind when I mention "newtype" (for lack of a better word).

[RossTate]

Haskell's newtype and ML-style module sealing were both designed for languages without subtyping, but the type-imports proposal specifically uses subtyping constraints on type imports. How are you planning to enable modules to seal export types with subtyping constraints?

For example, suppose I export a type $t with an upper bound struct (func (param $t) (result i32)), and I want to seal the type so that clients cannot access the other fields of the struct and have to treat it as essentially a black-box closure. How would I do that? (To be clear, the problem is that Haskell's newtype and ML-style module sealing involve creating a new value that does not satisfy the subtyping properties of the original value.)

[rossberg]

@RossTate, it is straightforward to extend ML-style sealing with bounds. In fact, ML already has equality bounds, we just add subtyping bounds. There is precedence for this, e.g., in Fisher & Reppy's Moby language (they called it partial type abstraction), as well as in Scala (although as often, Scala goes too wild, leading to decidability issues).

(To be clear, the problem is that Haskell's newtype and ML-style module sealing involve creating a new value that does not satisfy the subtyping properties of the original value.)

That is the case for Haskell's newtypes, where conversion is expressed by constructor application (though unless you introduce downcasts, that could be replaced by non-coercive type-level conversions that commute with subtyping).

ML-style sealing does not affect values, it's just a form of existential quantification (which is why, unlike Haskell, it works at higher order, too).

The idea of mixing the two approaches could be that newtype introduces a new nominal type that itself is a direct subtype of its representation type (and structurally identical, up to its type descriptor). Sealing then allows to hide arbitrary parts of that subtype relation.

[RossTate]

Okay, so you agree that newtype only solves the problem @lukewagner raises in #6 in easy cases where there is no subtyping constraint (and similarly where the exported type would not be used in subtyping constraints on other types). So it's not really a general-purpose solution to abstraction in the face of subtyping.

As for ML-style sealing, as you say it doesn't modify the values, but all its theoretical guarantees also rely on not being able to inspect values of types (except through the operations provided by their upper bounds). Casting, however, lets you do this, and the proposal lets any imported type be upcast to anyref and downcast to any type you want. So that doesn't seem to work either.

Can you lay out your plan for what a module trying to do what I described in #7 (comment) should do?

[rossberg]

There is no casting in this proposal. With GC types, which introduce it, casting is controlled by RTTs, which are intentionally explicit. A value's more specific type can only be discovered through downcasts if a module created the value with a respective RTT tag and exported that tag. Thereby, the provider of an abstract type has full control over possible downcasts and can prevent access to them as it sees fit.