B.3.5. Adjusted semantics for “assignment compatible” (⟺) - discussion

[chalin]

I am opening this issue as a place for discussion concerning B.3.5. Adjusted semantics for “assignment compatible” (⟺). cc: @munificent, @gbracha

[leafpetersen]

I was just reading over this section, this seems wrong to me. If I'm understanding this correctly, the result is that all nullable types are assignment compatible with all other non-nullable types. Consider two arbitrary types T and S. Are ?T and ?S assignment compatible? Per this proposed rule, it suffices to show that Null is assignment compatible with ?S, which either directly follows from the fact that Null is more specific than ?S, or indirectly via the adjusted assignment compatibility rule since Null is assignment compatible with Null (I'm assuming that the adjust assignment compatibility rule is intended to be symmetric). Am I misreading something, or missing some context?

[chalin]

Thank you for the feedback. The new case for <==>

?U ⟺ S iff Null ⟺ S ∨ U ⟺ S.

applies only when S is not of the form ?V. I agree that he proposal text isn't clear that the constraint "S is non-null" follows through to the new case description. Thanks for bringing that out. I've reworked the proposal text as follows:

we refine the definition of “assignment compatible” as follows: let T, S, V and U be any types such that ?V and ?U are in normal form, then we define T ⟺ S by cases:

• T ⟺ ?U iff T ⟺ Null ∨ T ⟺ U, when T is not of the form ?V

Otherwise the DartC definition holds; i.e., T ⟺ S iff T <: S ∨ S <: T.

Comment. It follows that ?V ⟺ ?U iff V ⟺ U.

Does this help clarify the situation?

[leafpetersen]

Hey Patrice - I'm still way lost in the weeds on this section. Concretely to your change, I think something went wrong in the drafting. You're trying to define when T <==> S, but the definition you've added doesn't mention S anywhere. This is the definition of T <==>S:

T ⟺ ?U iff T ⟺ Null ∨ T ⟺ U, when T is not of the form ?V

Note that it applies no matter what S is! Should U be related to S in some way?

I think I've also lost the thread on why you're doing this. I had thought I understood, in that it looked related to a problem that Lasse pointed out with a similar system that I kicked out for consideration at one point, but in reading your "more specific than" rules more closely, I no longer understand why you need this. Your motivating example is this:

class C2<T2 extends int> { ?T2 i2 = 1; }

The text claims that this is a warning - I don't understand why? If I understand the example correctly, the question boils down to whether or not ?T2 <==> int. Well, per the definition of assignability, it suffices to show that ?T2 <: int, and per the definition of subtyping, that is equivalent to showing that ?T2 << int. Per your extended "more specific than" rules in section B.3.1.b, it suffices to show that Null << int or T2 << int, so it suffices to show that T2 << int. But since T2 is bounded by int, this follows directly by the standard dart definition.

So we have that ?T2 <==> int, and no warning should be emitted. What am I missing?

I actually have some concerns with the proposed definition of "more specific than" (I'll file a separate issue), so perhaps there is a problem latent here, but I'm not sure that I see it given the current formulation.

[chalin]

You're trying to define when T <==> S, but the definition you've added doesn't mention S anywhere.

Sorry, I was in a Haskell function-definition-by-cases like mindset. I've just dropped T and S, so it reads "... we define ⟺ by cases: ...". You are also right that ⟺ is symmetric and I had only one of the cases written down. The revised definition text now reads:

• T ⟺ ?U iff T ⟺ Null ∨ T ⟺ U, when T is not of the form ?V
• ?V ⟺ S iff Null ⟺ S ∨ V ⟺ S, when S is not of the form ?U
• Otherwise the DartC definition holds; i.e.,
  T ⟺ S iff T <: S ∨ S <: T.

Essentially it is the same as in DartC except when one (and only one) of the arguments is of the (normal) form ?X.

The text claims that this is a warning - I don't understand why?

Let me take another look at my derivation and I'll get back to you. Note that I added the extra rules for << after having found the need to adjust the definition of ⟺. Maybe there is some kind of "feature interaction" between these two definitions that I had not anticipated.

[leafpetersen]

This may have been fixed by the textual fixes for #14, etc. I'll try to take another look soon.

The revised text here for assignability makes more sense. I don't quite understand the point of the T <==> Null clause of the disjunction in the assignability rule though. What does that add? If T is not of the form ?V, that seems to suggest that the only thing this clause covers are Object, dynamic, and subclasses of Null. The first two are already covered by the second clause, so then is this just about subclasses of Null (possibly just Null, assuming that Null is a final class)? Or am I missing something? If so, I think it might be clearer to break that out as a separate case:

Null <==> ?U T <==> ?U iff T <==> U, when T is not Null and not of the form ?V

or else just

T <==> ?U iff T == Null or T <==> U, when T is not of the form ?V

Or am I missing something about the effect of this rule?

[chalin]

I don't quite understand the point of the T <==> Null clause of the disjunction in the assignability rule though. What does that add? If T is not of the form ?V, that seems to suggest that the only thing this clause covers are Object, dynamic, and subclasses of Null.

~~The disjunct "T <==> Null" also covers the case of void; under the new definition of <==>, any nullable expression can be an argument to a void function's return statement.~~ [Edit: see https://github.com/chalin/DEP-non-null/issues/12#issuecomment-119317071]

(Note that Object is not assignable to Null.)

[chalin]

Your motivating example is this: class C2<T2 extends int> { ?T2 i2 = 1; }. The text claims that this is a warning - I don't understand why?

Please see the revised text of B.3.5. I dropped the generalizations and just stuck to illustrating why the assignment to i2 results in a static warning under DartC.

[chalin]

~~The disjunct "T <==> Null" also covers the case of void; under the new definition of <==>, any nullable expression can be an argument to a void function's return statement.~~

Actually, this was a special case that, in the end, I decided to pull out; given that even in DartC (where types are nullable by default), only expressions of type Null are accepted as arguments to return statements of void functions. So you might be right about the possibility of simplifying the T <==> Null term, though it seemed easier to motivate/explain using <==>.

[leafpetersen]

The revised text went wrong somewhere, unless I'm misunderstanding your intent. The type of 1.0 is double, not num. If you remove the ? annotations to get DartC code and run your example through the analyzer you'll get a bunch of static warnings because double and int are not assignment compatible, and hence double and T^int are not assignment compatible.

Do you really need to bring generics into it to motivate this example? If I understand what you're driving at, this is the point:

   int i = 42;
   int? j = i;

works without warnings, and so does

   num? i = 42;
   int? j = i;

but

   num i = 42;
   int? j = i;

gives a warning.

More substantively: I think I understand your motivation here. Basically, your observation is that if we return to your underlying model as union types, the natural notion of subtyping is via subsetting + subtyping (that is A <: B if each thing in A is a subtype of something in B. So the simple version of assignment compatibility as A <: B ^ B <: A essentially checks if there is a subset relation in either direction. That's fine for things like {Null, int} <==> {Null, num}, and for {Null} <==> {Null, num} and for {int} <==> {Null, num}, but you might argue that it should also be the case that {num} <==> {int, Null}, since a value of type int inhabits both types. So this is suggesting that the natural notion of assignability for union types in Dart might better be expressed as a kind of lower bound/intersection: A <==> B iff exists S in A, T in B s.t. S <==> T. But of course, this is too strong, since this would make all nullable types inter-assignable (as one would expect, since null does in fact serve as a common inhabitant of all nullable types, and hence the assignment could in fact succeed). So basically then, what you are aiming for is a modification of this that looks like: A <==> B iff exists S in A, T in B s.t. S <==> T, where S, T != Null.

Does that basically capture what you're aiming for? I should point out, by the way that this problem (insofar as it is a problem) already exists in Dart. Basically, there are types which have a common lower bound (and hence could potentially be valid to assign between) but which are nonetheless not inter-assignable.

// works without warnings
    List<int> ll = <int>[3];
    Iterable<int> ii = ll;

// works without warnings
    Iterable<num> ll = <int>[3];
    Iterable<int> ii = ll;

// warning
    List<num> ll = <int>[3];
    Iterable<int> ii = ll;

List and Iterable have a common subtype (List), but are not directly subtype related.

With classes, there doesn't seem to be a good way around this, since the set of classes is open ended and so we can't tell whether or not there might be a common lower bound without committing to a closed world assumption. I think your argument is that with nullability, the set of operators is constrained to ? and !, and so we can work make this work out directly by hacking the definition of assignability for them.

Is this a reasonable summary? Am I missing anything?

[chalin]

I think I understand your motivation here ... what you are aiming for is a modification ... like: A <==> B iff exists S in A, T in B s.t. S <==> T, where S, T != Null.

If you are now also convinced that the definition of ⟺ needs to be reworked in the presence of non-null types, then B.3.5 will have served its primary purpose.

As to the form of the redefinition, that can be further debated (and possibly backed with a formal semantics expressed, say, in Coq, which was next on my list). Our proposed redefinitions seem equivalent; but I think that the formulation given in B.3.5 might be slightly easier for end users to understand.

The revised text went wrong somewhere, ...

Right. Sorry that this silly error (last minute change in initializer type) distracted from the core discussion (over caffeination is no substitute for needed time off --- but that will soon be fixed!). Aiming for a better example, I had meant any initializer of type num; regardless, I have reverted that example back to use 1 (an int) as an initializer.

Do you really need to bring generics into it to motivate this example?

No but it gives (IMHO) the most convincing illustration that the definition of ⟺ needs to be adjusted. I.e., while some might want to debate whether ?int i = <num-expr> should be permitted, it seems quite counter intuitive to forbid, e.g., ?T i2 = 1 in class C<T extends int> { ?T i2 = 1; } (otherwise nullable fields of a generic type can only be initialized with null).

Is this a reasonable summary?

Thank you for your persistence in reviewing the material of B.3.5 despite the distractions. Yes I believe that we are on the same track.