Why is the argument of a cont_type a heap_type

[fgmccabe]

In the proposed spec interpreter, we have:

...

and func_type = FuncT of result_type * result_type
and cont_type = ContT of heap_type

My question is: why is cont_type defined this way. This syntactically permits invalid forms of continuation types. Why isn't it the same as a func_type:

and func_type = FuncT of result_type * result_type
and cont_type = ContT of result_type * result_type

[rossberg]

For one, because this avoids duplication: for most cont types of shape t1* → t2*, in practice you'll typically need function types of the same shape somewhere. This way, they can reuse the same definition.

Secondly, because there are in fact typing rules that need to form that sister function type from a given cont type, e.g., the typing rule for cont.new. If we couldn't simply extract a type index for it from the definition, then we'd generally need to synthesise auxiliary type definitions during validation, which would be gnarly — especially once recursive function types enter the picture, for which there wouldn't even be a uniquely determined rolled type to introduce. In the given formulation, the choice is fully determined by the definition of the cont type.

Malformed types or incorrect uses of type indices can occur in many other places (e.g., a function definition's type index not referring to a function type), so that isn't anything special.

[fgmccabe]

Should we not have some validation rules? E.g., a cont_type is only valid if its argument is an index type of a func_type definition?

[rossberg]

Yes, see here and here. :)

[fgmccabe]

ok. got it.

[fgmccabe]

Reopening, because the current design introduces an 'annoyance':
because cont types are the only type definition that introduces an auxiliary validation requirement like this, it makes validation significantly more difficult: we have to validate the type definitions in a group in two passes: one to read all the type definitions and a second to validate cont type definitions.

[tlively]

How is this different from e.g. a struct definition referring to another heap type via a reference-typed field? Ah, because of the validation rule that only function type indices are allowed.

Perhaps we can require that the function type is defined before the continuation type, similar to how we require that supertypes are defined before their subtypes, so their structure is already available to validate.

[rossberg]

That is a valid point. But of course, everything is a trade-off. The alternative of synthesising new type definitions during validation would be much worse in most implementations.

One hack to avoid the extra pass in this instance could be to restrict cont definitions such that they can only reference preceding indices, in the same way sub phrases do. However, that only works because the "shape constraint" is acyclic by nature. Such a restriction wouldn't scale to constructs that may indeed have bidirectional consistency conditions. Recursion generally is like that.

Having said that, don't you need an extra pass for checking sub within a recursive group anyway? Even though a supertype always is lexically preceding, it may reference types later in the group, and you at least need to know their subtyping bounds beforehand in the general case.

[fgmccabe]

Restricting cont types to acyclic will not work: if you use switching, then nearly every continuation will have a recursive type.

[tlively]

@fgmccabe, the idea is that only the edge from the cont type to its func type would have to go backwards, so you could still write this mutual recursion:

(rec
  (type $fA (param (ref null $cB)) (result (ref null $cB)))
  (type $fB (param (ref null $cA)) (result (ref null $cA)))
  (type $cA (cont (type $fA)))
  (type $cB (cont (type $fB)))
)

[tlively]

(But this should be moot due to the existing need for two passes that @rossberg mentioned.)

[fgmccabe]

Continuing (sic) my complaint: in V8, validating subtype correctness is a separate path in the validator. It is not exercised in cases not involving subtypes.
So, I will need to craft a special loop for recursive groups of types (inc singletons) that check a type definition: the only real check is that cont type is referencing a function type.