Chromium Code Reviews
|
|
Chromium Code Reviews
Issue
1236443002:
Core static semantics (Closed)
|
Created:
5 years, 5 months ago by Leaf Modified:
5 years, 5 months ago CC:
dev-compiler+reviews_dartlang.org Base URL:
git@github.com:dart-lang/dev_compiler.git@master Target Ref:
refs/heads/master Visibility:
Public. |
DescriptionCore static semantics checkpoint. First take on a core static semantics. Class typing is not done, but all of the core language is pretty well fleshed out. Fuzzy arrow types are handled, downwards inference on function types is modeled, and local variable type inference is modeled. Field lookup has not been specified yet.
I've split out the elaboration of the input syntax into the final program with runtime checks and suppressed that from the output for now.
BUG=
R=vsm@google.com
Committed: https://github.com/dart-lang/dev_compiler/commit/cdacc213ce7c5acc53676e19f54691fa1e56c2ee
Patch Set 1 #
Total comments: 43
Patch Set 2 : Address comments #Patch Set 3 : Update pdf #Patch Set 4 : Show elaboration rules #
Total comments: 4
Patch Set 5 : Address comments round 2 #
Messages
Total messages: 10 (1 generated)
leafp@google.com changed reviewers: + sigmund@google.com, vsm@google.com
https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.tex File doc/definition/strong-dart.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:131: checks. I admit, this surprised me a bit. I was expecting that \ecall and \eload would encode both normal and dynamic cases, and the only distinction would be what the type system does when it knows the receiver type. For example, var e = dload(o, m); dcall(e, arg); would be equivalent to: dynamic o2 = o; var e = o2.m; dynamic e2 = e; e2(arg); What is the intention behind these 2 explicit constructs? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:152: \text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{||} \ldots \\ not sure we get much from using a $\phi$ for ops :). How about simply $op$ or {\em op} instead? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:158: \alt \eprimapp{\phi}{\many{e}} \alt \ecall{e}{\many{e}} is \eprimapp only when you know it's a primitive type receiver (e.g. int.operator+) or also for any user operator (e.g. Vector.operator+)?
https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:23: subtype of the synthesized type, corresponding to an implicit downcast. As with the optional typing, I wonder if it's better to separate this out. We're currently a little inconsistent with how we handle this in the implementation - casts to generic types are warnings, likely to fail at runtime.... https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:32: \axiom{\yieldsOk{\Phi, \Delta, \extends{\Gamma}{x}{\tau}}{x}{\_}{x}{\tau}} There is type promotion - but perhaps that's orthogonal enough to ignore here. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:64: {\Arrow[-]{\many{\tau}}{\sigma}} Should this be \sigma_'_? https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:86: leaves this as a non-deterministic choice. Is this a step toward downward inference? https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:154: well-typed at the types given by the signature of the primitive. In Dart, these are really just syntactic sugar for regular methods. Perhaps we don't need primitives in this subset? Unless you want to model the weirdness around +, etc (int, int -> int and double, double -> double per hack in spec)? https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. What does dcall add if you allow e to be dynamic above? The rules / operations seem redundant. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:266: A dynamic load is well typed so long as the term is well-typed. Ditto? https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:300: } This reads a little odd to me ... seems to suggest that the synthesized type of e must exactly match the declared type of x. I would expect subtyping or assignability here. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:352: } Should \tau be required to be ground here and above? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.tex File doc/definition/strong-dart.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:128: Implicitly these are either inferred or filled in with dynamic. Is there a benefit to modeling inference here? It feels like it could be a 'pre-pass'. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:135: setter). This just simplifies the presentation a bit. Perhaps worth doing the same with loads for simplicity / consistency? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:170: \text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{vd}}} \\ Do you think we'll need to model implements as well? These will add requirements wrt covariant checks as well: class MyList implements List<int> { ... } and might get interesting in the presence of conflicts: class MyList extends ListBase<dynamic> implements List<int> { ... } https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:174: \text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{s} s here is effectively the body of main? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:193: \text{Type context ($\Delta$)} & ::= & \epsilon \alt \Delta, X \sub \tau \\ Define what X is in your list above? https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:209: treatment of dynamic. Do you need an explicit $-$? This is just standard / dynamic as top, right?
PTAL. I made fields entirely private, specified field and method lookup, and made a few other minor changes to address comments. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:23: subtype of the synthesized type, corresponding to an implicit downcast. On 2015/07/13 22:36:56, vsm wrote: > As with the optional typing, I wonder if it's better to separate this out. > We're currently a little inconsistent with how we handle this in the > implementation - casts to generic types are warnings, likely to fail at > runtime.... Yes, I have mental note to revisit this. We can have an explicit policy here (e.g. add a premise requiring tau to be a ground type), or we can make the rules parametric over a policy. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:32: \axiom{\yieldsOk{\Phi, \Delta, \extends{\Gamma}{x}{\tau}}{x}{\_}{x}{\tau}} On 2015/07/13 22:36:56, vsm wrote: > There is type promotion - but perhaps that's orthogonal enough to ignore here. Yes, I could formalize this, but it will take a fair bit of machinery, and I'm not sure it adds anything interesting. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:64: {\Arrow[-]{\many{\tau}}{\sigma}} On 2015/07/13 22:36:56, vsm wrote: > Should this be \sigma_'_? I think it *can* be, but not sure that it *should* be. I think it's a bit more standard to use the decorated type. It's similar to the rule for local variable bindings where we use the decorated type if given instead of using the more precise synthesized type. It's also a little more consistent with function declarations this way. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:86: leaves this as a non-deterministic choice. On 2015/07/13 22:36:56, vsm wrote: > Is this a step toward downward inference? This is downwards inference. It's specified in a slightly odd way to keep things readable. Basically, these rules allow missing argument and return types to be inferred from context. If we are in a function typed context and we are missing an argument type, this rule allows the argument type from the context type to be filled in. Alternatively, we can fill in the missing type with dynamic using the other rule. The typing rules are non-deterministic as to which we do: the function is well-typed so long as there is *some* derivation. In the implementation, we will likely choose to always use the context type if possible (that is, if the function is well-typed under that choice) in order to minimize the number of dynamic operations. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:154: well-typed at the types given by the signature of the primitive. On 2015/07/13 22:36:56, vsm wrote: > In Dart, these are really just syntactic sugar for regular methods. Perhaps we > don't need primitives in this subset? > > Unless you want to model the weirdness around +, etc (int, int -> int and > double, double -> double per hack in spec)? These really model the underlying primitive operations, not the methods named "+", etc. In the implementations (dart2js etc) these are what are implemented via "external" functions, or via inline JS. These aren't very important to us and I could leave them out, but it's a bit weird to have primitive types with no operations on them. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. On 2015/07/13 22:36:56, vsm wrote: > What does dcall add if you allow e to be dynamic above? The rules / operations > seem redundant. Basically I'm anticipating the dynamic semantics (which I haven't written in here yet, hence the confusion). The input program shouldn't have any dcall/dload constructs in it (though it doesn't matter if it does). The elaboration rules which add in the dynamic checks turn e.m when e is dynamic into dload(e, m), and similarly for dcall. In the dynamic semantics, dcall and e.m behave differently when m is not defined in e. Basically, e.m "segfaults" (or hard stops) and dcall throws an error (which we could choose to call no such method). The statement of soundness for expressions then takes the general form that if e elaborates to E, then evaluating E will never "segfault". That is, what we prove is that all potentially NSM producing lookups have been translated into dload/dcall operations which are prepared to deal with them, and all remaining loads and calls are guaranteed to succeed. This notion of soundness is what validates the compilation of Dart field load/method call directly into JS property load. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:300: } On 2015/07/13 22:36:56, vsm wrote: > This reads a little odd to me ... seems to suggest that the synthesized type of > e must exactly match the declared type of x. I would expect subtyping or > assignability here. The way it works here is a bit subtle, but I think it all works out. Remember that the rule is that if e checks at \opt{\tau} and synthesizes to \sigma, then \tau (if present) is a super type of \sigma. That is, the synthesized type is a subtype of the checked (context) type. So here, checking e checks that it is well-typed at \tau, and has some type \sigma which is a subtype of \tau. Then we check that x checks at \sigma and synthesizes to some \sigma' (and hence that \sigma' is a subtype of \sigma). Concretely, the variable rule does not apply when the checked type (\sigma) is not \_, so we apply the subsumption rule which says that x is well-typed as \sigma if x is well-typed at \_ and synthesizes to some \sigma' which is a subtype of \sigma. A variable x synthesizes to \sigma' if that is its declared type, so we end up checking exactly what you expect: that the type of e is a subtype of the declared type of e. If we wanted to loosen this to some kind of assignability, we could add some additional mechanism here. Note that the downcast rule can be applied instead of the subsumption rule here already though, so the assignment will still be valid if \sigma is a subtype of \sigma'. There will just be cast added during elaboration. In the implementation of course the uses of the subsumption and downcast rules get folded into the other rules via checkAssignment. This avoids the non-deterministic choice as to when to apply subsumption. But for the purposes of the specification, this simplifies the other rules substantially. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:352: } On 2015/07/13 22:36:56, vsm wrote: > Should \tau be required to be ground here and above? Yes. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:352: } On 2015/07/13 22:36:56, vsm wrote: > Should \tau be required to be ground here and above? Done. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.tex File doc/definition/strong-dart.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:128: Implicitly these are either inferred or filled in with dynamic. On 2015/07/13 22:36:56, vsm wrote: > Is there a benefit to modeling inference here? It feels like it could be a > 'pre-pass'. Maybe. I need to think about whether it can be separated out. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:131: checks. On 2015/07/10 00:20:58, Siggi Cherem (dart-lang) wrote: > I admit, this surprised me a bit. I was expecting that \ecall and \eload would > encode both normal and dynamic cases, and the only distinction would be what the > type system does when it knows the receiver type. > > For example, > > var e = dload(o, m); > dcall(e, arg); > > would be equivalent to: > > dynamic o2 = o; > var e = o2.m; > dynamic e2 = e; > e2(arg); > > > What is the intention behind these 2 explicit constructs? See my reply to Vijay's comment on dcall in the static semantics for details about this. Basically when I add the runtime checks in I want to distinguish between field loads/method calls which cannot fail, and ones which can. The latter turn into dcall/dload. The proof burden if we decide to prove soundness is to show that after elaboration, none of the remaining field loads can fail. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:135: setter). This just simplifies the presentation a bit. On 2015/07/13 22:36:56, vsm wrote: > Perhaps worth doing the same with loads for simplicity / consistency? Acknowledged. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:135: setter). This just simplifies the presentation a bit. On 2015/07/13 22:36:56, vsm wrote: > Perhaps worth doing the same with loads for simplicity / consistency? Done. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:152: \text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{||} \ldots \\ On 2015/07/10 00:20:58, Siggi Cherem (dart-lang) wrote: > not sure we get much from using a $\phi$ for ops :). How about simply $op$ or > {\em op} instead? Done. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:158: \alt \eprimapp{\phi}{\many{e}} \alt \ecall{e}{\many{e}} On 2015/07/10 00:20:58, Siggi Cherem (dart-lang) wrote: > is \eprimapp only when you know it's a primitive type receiver (e.g. > int.operator+) or also for any user operator (e.g. Vector.operator+)? The +/- etc syntax is just sugar, and I'm not modeling. These model the underlying operations on the primitive types that cannot be expressed in Dart itself (they are part of the underlying machine model). So + would operate on primitive integers, || on primitive bools, etc. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:170: \text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{vd}}} \\ On 2015/07/13 22:36:56, vsm wrote: > Do you think we'll need to model implements as well? These will add > requirements wrt covariant checks as well: > > class MyList implements List<int> { ... } > > and might get interesting in the presence of conflicts: > > class MyList extends ListBase<dynamic> implements List<int> { ... } Not sure that it's essential for the first pass. I don't think it adds anything deep, but it's true that it adds all sorts of unpleasant corner cases to work out. I can think about adding it in future if we want. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:174: \text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{s} On 2015/07/13 22:36:56, vsm wrote: > s here is effectively the body of main? yes. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:193: \text{Type context ($\Delta$)} & ::= & \epsilon \alt \Delta, X \sub \tau \\ On 2015/07/13 22:36:56, vsm wrote: > Define what X is in your list above? Should be type variable T. Fixed. https://codereview.chromium.org/1236443002/diff/1/doc/definition/strong-dart.... doc/definition/strong-dart.tex:209: treatment of dynamic. On 2015/07/13 22:36:56, vsm wrote: > Do you need an explicit $-$? This is just standard / dynamic as top, right? I'm defining two different relations: variant subtyping which is indexed by variance, and regular subtyping. I could make the - implicit, but then it becomes ambiguous which one I mean (albeit in a way that doesn't matter). Bit of a matter of taste, but I think the third rule in variant subtyping becomes very confusing if you leave it off. Also note that the function subtyping rule in the regular subtyping relation is parametric in the variance, so implicitly you do have the "-" indexed version of the rule as a hypothesis.
https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. On 2015/07/14 22:39:49, Leaf wrote: > On 2015/07/13 22:36:56, vsm wrote: > > What does dcall add if you allow e to be dynamic above? The rules / > operations > > seem redundant. > > Basically I'm anticipating the dynamic semantics (which I haven't written in > here yet, hence the confusion). The input program shouldn't have any > dcall/dload constructs in it (though it doesn't matter if it does). The > elaboration rules which add in the dynamic checks turn e.m when e is dynamic > into dload(e, m), and similarly for dcall. In the dynamic semantics, dcall and > e.m behave differently when m is not defined in e. Basically, e.m "segfaults" > (or hard stops) and dcall throws an error (which we could choose to call no such > method). The statement of soundness for expressions then takes the general form > that if e elaborates to E, then evaluating E will never "segfault". That is, > what we prove is that all potentially NSM producing lookups have been translated > into dload/dcall operations which are prepared to deal with them, and all > remaining loads and calls are guaranteed to succeed. This notion of soundness > is what validates the compilation of Dart field load/method call directly into > JS property load. Makes sense - I think it might be worth splitting the input language from the output of the translation in the future. Maybe even include a different term for the segfault cases (scall/sload) to avoid confusing input-language terms with the translated language terms.
lgtm https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:86: leaves this as a non-deterministic choice. On 2015/07/14 22:39:49, Leaf wrote: > On 2015/07/13 22:36:56, vsm wrote: > > Is this a step toward downward inference? > > This is downwards inference. It's specified in a slightly odd way to keep > things readable. Basically, these rules allow missing argument and return types > to be inferred from context. If we are in a function typed context and we are > missing an argument type, this rule allows the argument type from the context > type to be filled in. Alternatively, we can fill in the missing type with > dynamic using the other rule. The typing rules are non-deterministic as to > which we do: the function is well-typed so long as there is *some* derivation. > In the implementation, we will likely choose to always use the context type if > possible (that is, if the function is well-typed under that choice) in order to > minimize the number of dynamic operations. So, if my expr is: (e) => e.foo and my contextual type is: int => int would that type check? The first rule appears to apply here. Per #203, I think we might want to disallow it. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. On 2015/07/14 23:59:21, Siggi Cherem (dart-lang) wrote: > On 2015/07/14 22:39:49, Leaf wrote: > > On 2015/07/13 22:36:56, vsm wrote: > > > What does dcall add if you allow e to be dynamic above? The rules / > > operations > > > seem redundant. > > > > Basically I'm anticipating the dynamic semantics (which I haven't written in > > here yet, hence the confusion). The input program shouldn't have any > > dcall/dload constructs in it (though it doesn't matter if it does). The > > elaboration rules which add in the dynamic checks turn e.m when e is dynamic > > into dload(e, m), and similarly for dcall. In the dynamic semantics, dcall > and > > e.m behave differently when m is not defined in e. Basically, e.m "segfaults" > > (or hard stops) and dcall throws an error (which we could choose to call no > such > > method). The statement of soundness for expressions then takes the general > form > > that if e elaborates to E, then evaluating E will never "segfault". That is, > > what we prove is that all potentially NSM producing lookups have been > translated > > into dload/dcall operations which are prepared to deal with them, and all > > remaining loads and calls are guaranteed to succeed. This notion of soundness > > is what validates the compilation of Dart field load/method call directly into > > JS property load. > > Makes sense - I think it might be worth splitting the input language from the > output of the translation in the future. Maybe even include a different term for > the segfault cases (scall/sload) to avoid confusing input-language terms with > the translated language terms. It's the same thing (I think), but it might be a little clearer to think about if you expressed this as e(x) is typed if e is dynamic and dcall(e, x) is typed. https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... doc/definition/static-semantics.tex:8: term being checked. The optional type $\opt{\tau}$ is the type against which Is this also the contextual type? If so, maybe define it explicitly here. You use the term below without defining. https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... doc/definition/static-semantics.tex:18: such rules apply in the cast that we have contextual type information, subject 'cast '-> 'case' ? This sentence reads a little awkwardly.
https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:86: leaves this as a non-deterministic choice. On 2015/07/15 18:25:34, vsm wrote: > On 2015/07/14 22:39:49, Leaf wrote: > > On 2015/07/13 22:36:56, vsm wrote: > > > Is this a step toward downward inference? > > > > This is downwards inference. It's specified in a slightly odd way to keep > > things readable. Basically, these rules allow missing argument and return > types > > to be inferred from context. If we are in a function typed context and we are > > missing an argument type, this rule allows the argument type from the context > > type to be filled in. Alternatively, we can fill in the missing type with > > dynamic using the other rule. The typing rules are non-deterministic as to > > which we do: the function is well-typed so long as there is *some* derivation. > > > In the implementation, we will likely choose to always use the context type if > > possible (that is, if the function is well-typed under that choice) in order > to > > minimize the number of dynamic operations. > > So, if my expr is: > > (e) => e.foo > > and my contextual type is: > > int => int > > would that type check? The first rule appears to apply here. Per #203, I think > we might want to disallow it. As currently specified, it will type check, and will reify as dynamic -> dynamic. The example in #203 would typecheck, but x, y, and the return type would all be filled in with int (hence no dinvokes). Basically, these rules allow for the contextual type to be used to fill in the missing argument types, but don't require it (if the body can't be typed using the more specific types, the arguments can be left as dynamic). We could choose to disallow the dynamic case - this would simplify the implementation in fact. The downside is that more programs would get rejected. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. On 2015/07/15 18:25:34, vsm wrote: > On 2015/07/14 23:59:21, Siggi Cherem (dart-lang) wrote: > > On 2015/07/14 22:39:49, Leaf wrote: > > > On 2015/07/13 22:36:56, vsm wrote: > > > > What does dcall add if you allow e to be dynamic above? The rules / > > > operations > > > > seem redundant. > > > > > > Basically I'm anticipating the dynamic semantics (which I haven't written in > > > here yet, hence the confusion). The input program shouldn't have any > > > dcall/dload constructs in it (though it doesn't matter if it does). The > > > elaboration rules which add in the dynamic checks turn e.m when e is dynamic > > > into dload(e, m), and similarly for dcall. In the dynamic semantics, dcall > > and > > > e.m behave differently when m is not defined in e. Basically, e.m > "segfaults" > > > (or hard stops) and dcall throws an error (which we could choose to call no > > such > > > method). The statement of soundness for expressions then takes the general > > form > > > that if e elaborates to E, then evaluating E will never "segfault". That > is, > > > what we prove is that all potentially NSM producing lookups have been > > translated > > > into dload/dcall operations which are prepared to deal with them, and all > > > remaining loads and calls are guaranteed to succeed. This notion of > soundness > > > is what validates the compilation of Dart field load/method call directly > into > > > JS property load. > > > > Makes sense - I think it might be worth splitting the input language from the > > output of the translation in the future. Maybe even include a different term > for > > the segfault cases (scall/sload) to avoid confusing input-language terms with > > the translated language terms. > > It's the same thing (I think), but it might be a little clearer to think about > if you expressed this as e(x) is typed if e is dynamic and dcall(e, x) is typed. > > Done. https://codereview.chromium.org/1236443002/diff/1/doc/definition/static-seman... doc/definition/static-semantics.tex:213: arguments are well-typed at any type. On 2015/07/14 23:59:21, Siggi Cherem (dart-lang) wrote: > On 2015/07/14 22:39:49, Leaf wrote: > > On 2015/07/13 22:36:56, vsm wrote: > > > What does dcall add if you allow e to be dynamic above? The rules / > > operations > > > seem redundant. > > > > Basically I'm anticipating the dynamic semantics (which I haven't written in > > here yet, hence the confusion). The input program shouldn't have any > > dcall/dload constructs in it (though it doesn't matter if it does). The > > elaboration rules which add in the dynamic checks turn e.m when e is dynamic > > into dload(e, m), and similarly for dcall. In the dynamic semantics, dcall > and > > e.m behave differently when m is not defined in e. Basically, e.m "segfaults" > > (or hard stops) and dcall throws an error (which we could choose to call no > such > > method). The statement of soundness for expressions then takes the general > form > > that if e elaborates to E, then evaluating E will never "segfault". That is, > > what we prove is that all potentially NSM producing lookups have been > translated > > into dload/dcall operations which are prepared to deal with them, and all > > remaining loads and calls are guaranteed to succeed. This notion of soundness > > is what validates the compilation of Dart field load/method call directly into > > JS property load. > > Makes sense - I think it might be worth splitting the input language from the > output of the translation in the future. Maybe even include a different term for > the segfault cases (scall/sload) to avoid confusing input-language terms with > the translated language terms. Yes, this is reasonable. I need additional mechanism for the dynamic semantics anyway. I'll either split out these terms, or mark them in some way as just part of the translation/dynamic semantics. https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... File doc/definition/static-semantics.tex (right): https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... doc/definition/static-semantics.tex:8: term being checked. The optional type $\opt{\tau}$ is the type against which On 2015/07/15 18:25:34, vsm wrote: > Is this also the contextual type? If so, maybe define it explicitly here. You > use the term below without defining. Done. https://codereview.chromium.org/1236443002/diff/60001/doc/definition/static-s... doc/definition/static-semantics.tex:18: such rules apply in the cast that we have contextual type information, subject On 2015/07/15 18:25:34, vsm wrote: > 'cast '-> 'case' ? This sentence reads a little awkwardly. Done.
still lgtm
Message was sent while issue was closed.
Committed patchset #5 (id:80001) manually as cdacc213ce7c5acc53676e19f54691fa1e56c2ee (presubmit successful). |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
