Andreas Rossberg

As for a more structured solution, I suggested experimenting with type imports to prune the type definitions not relevant to each module itself. I could imagine this might help significantly,...

A correctly compiled program should never mismatch the length of a segment. That would always be the symptom of a compiler bug, and non-trapping behaviour can't help with that. I...

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...

Yes, see [here](https://github.com/WebAssembly/stack-switching/blob/main/proposals/stack-switching/Explainer.md#types) and [here](https://github.com/WebAssembly/stack-switching/blob/5010b4ea7e7fc4d8db3f0415df7437cd23eeafc4/interpreter/valid/valid.ml#L181). :)

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...

Agreed with @nomeata: only makes sense to do this if we do all the bitops – I changed the issue title accordingly. Also, FWIW, there is no `~` op in...

> In essence, the possible return types of a function are "bigger" than the possible input types to the function. This results in the lack of a mathematical property called...

> So in a scripting language, what do you do with `let x = invoke(a, b, c);`? What is the type of `x`? In all programming languages I can think...

@jdegoes, just a nit: typing rules apply to all expressions, terms = expressions, so these are terms and they have types. There are merely no variables of these types, as...

It _does_ have a type in the domain of expressions, but not values, so I'd rather say something like > The result of a function is not a plain value...