-
Notifications
You must be signed in to change notification settings - Fork 24
Flow Sensitivity #42
Comments
How does nominal types solve this issue? |
I'm not sure how this example relates to the multivalue proposal (or WebAssembly more generally), and it seems to assume quite a bit of typing machinery that WebAssembly does not have today. Could you perhaps sketch out what features would have to be included in WebAssembly for this example to become possible and also reframe the example to use WebAssembly rather than Java? |
I just thought y'all might appreciate some foreshadowing on what kind of reasoning it will take for WebAssembly to ensure that the values from a
Discussions like #41 talk about the tradeoffs between using local variables and using the stack, with the multivalue proposal making the stack much more usable. Other low-level type systems, like typed assembly languages, use reasoning more like the stack than like local variables. The reason is that the type of the stack is a snapshot in time of multiple values, whereas the type of a local variable stays fixed and only talks about one value. To get a sense of what that means, consider the line
Certainly. This is about looking ahead, specifically about where WebAssembly would need to go to be able to type-check the compilations of major type-safe languages without inserting many dynamic casts (if that's where it wants to go).
Theoretically speaking, this is orthogonal to nominal vs. structural types. Instead, it's more related to existential types. Practically speaking, I don't believe there exists even a research compiler that has been able to put the relevant theory for structural types to practice on a real language. On the other hand, for nominal types there already exists an algorithm that can automatically type-check the above example without any additional type annotations within the body of Regardless, I didn't bring this up as part of that debate. I just wanted to give y'all a heads up rather than have y'all later wish the issue had been mentioned before. I also wanted y'all to have a glimpse of what we meant by "fancy types", and why we opted to present y'all with an MVP that was forwards-compatible with fancy types but didn't itself require fancy types—a question that was raised during one of the meetings. |
Thanks, this makes more sense to me now :) |
Cool. Thanks for helping me realize how unclear I was being. |
To get a sense of what that means, consider the line assert elem_type ==
Integer.rtt;. Right before this line, the snapshot-in-time-type is "[ints
: Array, elem_type : RTTI] where ints' element type equals the type
represented by elem_type". Right after that line, we learn that elem_type
is equal to the RTTI for Integer, so we get the snapshot-in-time-type "[ints
: Array, elem_type : RTTI] where ints' element type equals the type
represented by elem_type *and* the type represented by elem_type equals
Integer". By combining these two equalities relating the two distinct
variables ints and elem_type, we realize that ints is an Array whose
element type equals Integer in this snapshot-in-time-type.
The assertion that "int's element type = the type represented by elem_type"
is not representable in the notation you are using.
Makes me want to reformulate it using logical variables .. :)
…--
Francis McCabe
SWE
|
Yeah, there are a number of ways to express this formally. The most common is constrained existential types, but there are others that might be a better fit for WebAssembly (if we go down this path). Other VMs have tackled this by baking in language primitives, so by not taking that path y'all have embarked on a fairly unworn path. |
Here is some food for thought that might be relevant to discussions such as in #41. Low-level type systems generally need to at some point incorporate multi-value flow-sensitivity. That means that a branch taken on one value needs to be able to affect the operations you can do on other values on the context.
Here's an example for supporting Java/C# (that normally wouldn't be written this way but which would be produced by inlining):
At the low level, this turns into:
Notice that, in order for this to type check, after branching on
elem_type == Integer.rtt
we need to realize that this means the references contained inints
necessarily have anint_value
field even thoughelem_type == Integer.rtt
has no direct reference toints
.Without multi-value flow-sensitivity, you can only get the following to type check:
That is, we have to cast every reference retrieved from
ints
toInteger
even after asserting that its element type is the correct type. To make matters worse, if you don't have multi-value flow-sensitivity, there's no way to enforce the expectation that a surface-levelInteger[]
only containsInteger
references, so you'll have to cast the result ofint[i]
even whenints
has surface-level typeInteger[]
.(Note: all of this is independent of covariant arrays, so feel free to ignore that additional complexity when pondering this food for thought.)
So when considering design options, you might want to think of which options better support multi-value flow-sensitivity.
The text was updated successfully, but these errors were encountered: