Subtyping for continuation types

[titzer]

With GC now at phase 4, soon we will want to rebase work here on top of it. Wasm GC introduces declared subtyping for functions, structs, and arrays. Does it seem reasonable to allow declared subtyping on continuation types? The main implication here is that a continuation will need a dynamic type tag for casting.

[rossberg]

I agree that we probably want to allow (declared) subtyping on continuations. However, it is important to note that this by no means implies that we also support downcasts on them. Those are two completely separate features, and I want to stress again that we don't want to force the cost of the latter on every reference type.

For continuations in particular, I don't think we want to support the latter. It would be rather costly, e.g., getting in the way of an allocation-free implementation strategy via fat pointers, since suspend/resume generally produce a different type for each continuation of the same stack (and this type is in fact determined by the handler). At a minimum, that would force the fat pointer to have a third word.

If a program absolutely needs to downcast over continuations, then it can still achieve that easily by wrapping them into a struct. That way it remains pay-as-you-go.

[tlively]

No disagreement that subtyping and casting are technically separable, but the value of subtyping seems significantly diminished if you cannot also do a cast to recover the specifics of a value. What is a situation where subtyping is useful without casting?

[rossberg]

The usefulness of subtyping is independent from downcasts, it's simply a form of type polymorphism. Not all languages with subtyping even have casts. The only reason you typically need downcasts is to work around limitations of a type system, e.g., lack of generics or lack of variants, which you then encode with top type (or other common super type) + downcasts. Obviously, these limitations apply to Wasm, but they hardly matter for the common use case of continuations (and in the rare case they do there is a simple workaround).

[rossberg]

PS: FWIW, our implementation in the reference interpreter already supports subtyping on continuation types, per subtyping on the underlying function types as you would expect. For example, the following is accepted:

(module
    (type $f1 (sub (func (result anyref))))
    (type $f2 (sub $f1 (func (result eqref))))
    (type $c1 (sub (cont $f1)))
    (type $c2 (sub $c1 (cont $f2)))
)