-
Notifications
You must be signed in to change notification settings - Fork 695
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Understanding the type system for br
s
#677
Comments
For the first two, consider their equivalent simplifications which are valid. The consumer is not expecting values so the excess are discarded.
Correction: The last case is invalid because the fall-through value is empty but a single value is expected.
I demonstrated the multiple-value type system in WebAssembly/wabt#66 and proved it fits a single pass compiler, and the break operators accept a single argument expression. If you want to understand how the current type system could extrapolate to multiple value then this might help. It might be a little confusing that an arity count has just been added to the very common break operators. I argued against it. Go figure. I no longer think it is productive to explore these issues. There is discussion of removing the void type, in which case no value could be implicitly discarded, and the issue goes away. An expressionless encoding would achieve the same. |
Sorry, that just makes me more confused. What is a "simplification"? Is it just to explain the concept, or is that how a checker would actually work? All I'm looking for here is the concrete rules of how I assign a type to |
|
Thanks! This looks fairly complex - I'm not surprised that I couldn't figure it out just by reading the tests ;) How did we arrive at this system - where was the design discussed? I see no mention of a |
@kripken The spec is defined in terms of a top down type system so does not need to even reference the type |
A couple of clarifications and corrections:
The most interesting ones of those constraints are:
A type T is a subtype of U if and only if T = U, or U is void. Note in particular that the result type of As for your original question: the |
@rossberg-chromium I think I'm still confused. So
Hence if a block has a a. look at ? I guess it has to be I may still be missing something big here, but a second question: It seems like the above rules imply that the type of a node can change if it is moved around - e.g. the exact same |
[Reposting, because Github garbled the quotes badly, and editing can't fix it?]
Well, unconstrained means that there is nothing to check. Is that more
Now you are asking about an algorithm. Technically, a type system is not, There are various algorithmic ways to check these constraints, but
Yes. That is the nature of any form of type polymorphism (parametric, |
Ok, thanks, I think I get it now.
But is that complexity necessary here? Instead of
We could instead have a. blocks have the type of the values that brs to them have, or if they have none, that of their last expression, and By not requiring that blocks have the type of their last expression, we can let brs always have the empty type. So a br at the end of a block has the empty type, and also if there were something after it in that block (it wasn't the last anymore) it would still have the empty type. In other words, we trivially know the type of a br, and we also know it won't change if we move it around. I believe these two are equivalent in practice, I think the only difference is the internal type of the br. |
Not sure I understand. A block has to yield a consistent type, no matter how it's exited. So the value from its final expression must have the same type as any associated break argument. Something like
cannot possibly be allowed. Also, the last expression does not affect type checking complexity. Either way, you have to check that all associated break arguments are consistent, the last value is just one more expression to consider (and any The only alternative to the current design would be to remove break arguments entirely, and require all blocks that are targeted by a break to have type void. Not entirely unreasonable, but a somewhat sad limitation for an expression language. |
Perhaps I wasn't clear enough, sorry. In 1-2 and a-b I wasn't specifying all the validation. I was specifying how the type can be determined, assuming correctness. Full validation needs a tiny bit more work. Specifically, 1-2 also require 3: all breaks to the block have the same value type (but tolerate inconsistency if it is not consumed; see bottom of this post) and a-b also require c: all breaks to the block have the same value type, and also the last element in the block must have the same type As a result, your example that should fail to validate does in fact fail to validate in a-c. (I think: your example has 7 open parens, but only 6 closing, so maybe it's missing one in a way that I guessed wrongly.) The issue here isn't complexity in the sense of how much work needs to be done. It's how hard it is to understand the type system. Obviously subjective. But in yours, the type of brs depends on their location. In mine, the type of brs is trivial and fixed. And there is additional complexity for blocks as well that feels unnecessary. Consider these two examples:
(only difference is adding a result in the second) In your type system, the second fails. In mine, both fail. I claim that this is less complex, as in mine, whether a block is valid or not does not depend on the block's location. You can move the block around, it doesn't matter. And these examples, shouldn't both fail? We have here a block with a branch of an i32, so the presumed type should be i32; however, br_if is an instruction that may not branch, and if it does not, we are returning a nop, in effect. That's clearly wrong, isn't it? Or is there some value to allowing it to validate, and only fail lazily if the wrongness is used?
I certainly hope not! :) I think there is an alternative, as described above. Unless I missed something... |
@kripken Right, you're describing something similar to what @jcbeyler brought up here: WebAssembly/spec#179. Then the type checking was tightened here: WebAssembly/spec#180. Then after much discussion was loosened here: WebAssembly/spec#271. From the last link:
(this space so the quote above doesn't get merged with the quote below)
I don't think that's the right way to think of it.
No, since there is a control flow path that returns no value (the |
Okay, I believe your suggestion boils down to whether we allow implicit dropping for break arguments. That is indeed the very issue that @binji linked to. FWIW, Luke and I have recently discussed introducing an explicit |
@rossberg-chromium A block does not have 'to yield a consistent type, no matter how it's exited'. It could yield no values (void), one value (i32,i64,f32,f64), two values or more, and the None type, all on different exit paths and so long as the value(s) are not consumed it could work just fine for wasm. The constraint in wasm could be that only a single consistent type i32,i64,f32,f64 can be consumed either as a single value type. All the exit paths from a block can be handled in the same manner by the type system, and the fall-through and break expression do not have to be handled differently. This is proven by demonstration WebAssembly/wabt#66 and the type checking was not complex and perhaps a page or two of code. Happy to work through this with anyone wanting to understand the perspective, but I now suggest an expressionless encoding which has a much simpler type system and there is no need to reason about |
@binji: thanks for the links! Ok, it sounds like this issue is documented in various issues in the spec repo? I'll try to read all of those. (However, it's a lot to read. As in the first part of this issue, I think it would be valuable to have a single summary of the type system somewhere.) I totally understand if you guys don't want to discuss this with me further until I read all those issues in depth, so I guess we can close this. But after a first read through them, I don't see where what I and @jcbeyler suggested reduced compositionality in an important way? A direct example would be helpful. Is it one of the many new tests added in that last PR? I'm not sure what to look for. For example, in the following quote is something that the proposal would indeed make no longer validate, yet it's clearly not helpful that it does validate? To not validate it would lose nothing of value.
But what does it mean for that block to have void type? I am arguing that block should not be valid at all. It's a logical impossibility, it can flow out either an i32 or a nothing. Why should we wait to see if it's used to give an error is what I'm asking. |
@kripken For the example in question, and noting that the constant condition is not seen by the type system, the block can return type |
@JSStats: What I am saying is that allowing a block to have a type that is the union of Unless there is a useful use of them, but I don't see one yet. |
@kripken It is a useful as being able to discard unused values in expression based language. The utility can be demonstrated in technical terms of encoding efficiency. e.g |
On 29 April 2016 at 23:38, JSStats notifications@github.com wrote:
No, it can't. If you want to be able to think of Wasm as a stack machine, However, that does not mean that the type system does not allow the From the POV of a traditional evaluator that's mostly isomorphic to your |
@rossberg-chromium See the demonstration at WebAssembly/wabt#66 which supports different types on all the block exits and still compiles to a stack machine in a single pass, and it balances the stack! It's been demonstrated, it works fine, it's relatively simple. A multiple-pass runtime compiler will know before code generation that the type is a complex union and that it is not consumed, it could effectively drop all values. Practical optimizing compilers will not be emitting code in one pass, just converting to an SSA form, and when they find complex unions just drop the definitions as it knows they are not consumed. The generated code will be every bit as good as if there were explicit A single-pass runtime compiler might have emitted some code for some exits before it discovers that the type is a complex union and can not be validly consumed. A compiler to a stack machine just has to balance the remaining exits by dropping values or filling as necessary. |
@JSStats, as I said, different isomorphic interpretations are possible. However, the crucial meta constraint is that the type system can only correctly support a stack machine if any use of union types is so restricted that you can still reformulate the rules without them. |
@JSStats: Fair point, in rule (c) above it should be amended to "all brs must have the same returned value type, and if that is a concrete type, the last element in the block must match it." (Then the last element can have its value discarded if necessary.) @rossberg-chromium: Where did this new constraint of "support a stack machine" come from? |
@kripken If 'rule (c)' is just a rule for cases in which the value can be consumed then yes. If it implies that it is invalid for any of the break values to have different types then this would not be necessary. For example the follow could be valid so long as the result is not consumed:
and could be seen as a more efficient and less verbose encoding of
All the break value expressions could just be moved above the |
@JSStats: I see, thank you. Those examples helped me understand why this flexibility is useful. |
I guess I still don't understand the type system for
Why does it fail? The output of the block is not consumed, so it's valid for it to have an invalid type, isn't it? |
It needs to fail because the |
Oh, thanks! Heh, I guess that's what I get for trying to do this at 10pm... :) |
This was mostly clarification, closing. |
I can't figure out why these three should pass (all from spec test suite):
Is there documentation for the type system somewhere that I should read, that would explain why the last is bad but not the first two? Basically, documentation for the types of
br
s in particular?I've mostly just looked at the spec tests and gotten things working, but I'm trying to enable complete validation testing in binaryen, and I see failures that suggest I have no idea how this type system actually works :)
The text was updated successfully, but these errors were encountered: