Messages that include union types are pretty much impossible to read

[stevemessick]

Username: kasperl

The error / hint messages that include union types are pretty much impossible to read and understand.

The argument type '{BadInterfaceType,BadTypedefType,TypedefType,MalformedType,InterfaceType}' cannot be assigned to the parameter type 'GenericType'

It's not clear that this is really a union type.
////////////////////////////////////////////////////////////////////////////////////
Editor: 1.7.0.dev_02_00 (2014-09-10)
OS: Linux - amd64 (3.13.0-35-generic)
JVM: 1.7.0-google-v6

projects: 1

open dart files: 3

auto-run pub: true
localhost resolves to: 127.0.0.1
mem max/total/free: 1778 / 887 / 304 MB
thread count: 29
index: [737502 locations, 265 sources, 80240 elements]

---

Attachment:
screenshot.png (366.55 KB)

[danrubel]

cc @kasperl.
Removed Priority-Unassigned label.
Added Priority-Medium label.

[bwilkerson]

Set owner to [email protected].
Added this to the 1.7 milestone.
Removed Priority-Medium label.
Added Priority-High, Analyzer-UX labels.

[DartBot]

This comment was originally written by [email protected]

---

Ideas for a better [toString()] for union types?

We currently have

  {A,B}

Some languages use

  A|B

We could go with something more verbose like

  A or B

or

  some type in {A,B}

or

  union of A and B

or

  one of A or B

or

  an unknown type that is either A or B

or ???

For the hint message itself, we could change it completely to something like

  none of the possible argument types here (A or B) can be assigned to the parameter type C

[bwilkerson]

Issue #20957 has been merged into this issue.

[peter-ahe-google]

I suggest you avoid the concept of union types altogether, and pick concrete types that leads to problems. For example:

Instead of saying:

The argument type '{BadInterfaceType,BadTypedefType,TypedefType,MalformedType,InterfaceType}' cannot be assigned to the parameter type 'GenericType'

Say something like this:

The type of the expression "expr" can have the type "MalformedType" which isn't assignable to the type of "foo", "GenericType".

At the same time, I think it is important to realize that "parameter" vs "argument" is a distinction you shouldn't expect most programmers to get.

[DartBot]

This comment was originally written by [email protected]

---

Added Started label.

[DartBot]

This comment was originally written by [email protected]

---

I've changed the definition of union-type subtyping to make such messages much less common, and I've changed the union-type string representation to be more user friendly.

The definition of union-type subtyping is now

  {A1, ..., An} <: B

if

  Ai <: B

for any [i]. Before we required this for all [i], which seems more sound, but does not really have the desired effect because assignment compatibility is defined by

  A <=> B

if

  A <: B or B <: A

and we define

  A <: {B1, ..., Bn}

when

  A <: Bi

for any [i]. CL: https://codereview.chromium.org/578643004/

I changed the string representation from

  {A1, ..., An}

to

  (A1 or ... or An)

which is hopefully more intuitive. CL: https://codereview.chromium.org/576403002

[peter-ahe-google]

This doesn't sound like a solution to me. The diagnostic message talks about a singular type, and you jam in multiple types.

You need to explain to the user what is wrong, and why it is wrong. Reusing a diagnostic message doesn't seem to accomplish this.

---

cc @lukechurch.

[DartBot]

This comment was originally written by [email protected]

---

OK, looks like we're stuck then. As I see it, there are three options:

1. we expect users to learn a simple, intuitive new concept.
2. someone other than me specifies a union type UI and we agree on it.
3. we eliminate union types.

Details
=======

1. we expect users to learn a simple, intuitive new concept. We don't
   have to use the term "union types", and instead of the set notation
   [{A,B}] we can use the intuitive or-notation [(A or B)]. But users
   have to learn that code like

  var x;
  if (c) {
    x = new A();
  } else {
    x = new B();
  }
  // Here [x] has type [(A or B)].

results in the type of [x] being [(A or B)]. This seems reasonable to
me, but I may be biased.

Outstanding issues here include the UI for examples like

  class A {
    int m(int x) => x;
  }
  class B {
    double m(double x) => x;
  }
  f() {
    var x;
    if (c) {
      x = new A();
    } else {
      x = new B();
    }
    // Here [x] has type [(A or B)]. But what is [x.m]?
  }

where there are conflicting possibilities for the method [m]. The
current approach is to say that

  x.m : ((int or double)) -> (int or double)

because this works well in the following common case:

  var x;
  if (c) {
    x = [0];
  } else {
    x = [0.5];
  }
  // Here [x] has type [(List<int> or List<double>)], and [x.[]] has
  // type [(int) -> (int or double)].

Alternative approaches include saying that

  x.[] : ((int) -> int or (int) -> double)

but this is probably much harder to fit into the current
implementation: I don't think there is any notion of a field or method
lookup resolving to more than one thing.

1. someone other than me specifies a union type UI and we agree on
   it. It can't be me because I think telling the user that the type can
   be [(A or B)] is fine, so I don't expect I'll come up with a solution
   that will make everyone happy. Adding a note to the editor docs
   somewhere, explaining the intuitively obvious [(A or B)] notation
   seems like enough to me; indeed, the editor UI currently presents
   function types using the arrow notation which is not part of the Dart
   language syntax and no one complains. I expect the [(A or B)] notation
   to be similarly received; the set notation was probably a mistake.
2. we eliminate union types. The simple version of this is that we
   just back out all the union-types related changes. A more complicated
   version of this is that we make union types disappear before they
   reach the user, but still use them internally to motivate hints. One
   way to make them disappear, while still potentially getting some of
   their benefits, is to collapse them using a custom least upper bound
   (lub). I say "custom" because the spec lub is flawed (recall the
   [EfficientLength] problem:
   https://code.google.com/p/dart/issues/detail?id=19425).

However, using a custom lub would almost surely have the effect of
generating some incorrect hints . For example:

  var x = 0;
  if (0 < 1) {
    x = 'lalalala';
  }
  // Here [x : (int or String)].
  if (0 < 1) {
    // If we use a lub to eliminate the union type then [x : Object]
    // here and we get an incorrect hint.
    return x.allMatches('la');
  }

Of course, I think there are some nice ways out here, but they are
very controversial:

• expect the user to understand that our analysis is not perfect and
    that they need to help us by rewriting their code, e.g.:

    var x = 0;
    if (0 < 1) {
      x = 'lalalala';
      // Here [x : String], so no problem.
      return x.allMatches('la');
    }
    // Here [x : (int or String)].

• give the user an escape hatch for when the analysis fails. The
    solution I prefer here is making [dynamic] mean something different
    from [var]. Namely, [dynamic] means "leave me alone I know what I'm
    doing". In this case they change their code to

    dynamic x = 0;
    if (0 < 1) {
      x = 'lalalala';
    }
    if (0 < 1) {
      return x.allMatches('la');
    }

  and the hint goes away because [x] is marked as "anything
  goes".

---

Added Waiting label.

[bwilkerson]

Re-writing the relevant messages shouldn't be that hard. For example, instead of the original

  The argument type '{BadInterfaceType,BadTypedefType,TypedefType,MalformedType,InterfaceType}'
  cannot be assigned to the parameter type 'GenericType'

what if we were to say

  None of the possible types of the argument can be assigned to the parameter type 'GenericType'

and then fix the hover text so that the propagated type displays, much like you were suggesting for error messages, as

  One of BadInterfaceType, BadTypedefType, TypedefType, MalformedType, or InterfaceType

[peter-ahe-google]

I don't think there's anything intuitive about "union" types. Claiming that they're simple and intuitive doesn't make it so, and we deliberately avoided these kinds of things to keep the Dart type system simple.

Regarding Brian's suggestion, I'd like to understand how that information will be presented in the command line version of the analyzer.

[DartBot]

This comment was originally written by [email protected]

---

There are a lot of things getting mangled together here that need to be separated.

I also think that we're not getting anywhere near as much user value out of the underlying technology here as we could be doing.

I'll send out a vc invite to discuss.

[DartBot]

This comment was originally written by [email protected]

---

@ahe

I don't think there's anything unintuitive about "union" types. Claiming that they're not simple nor intuitive doesn't make it so, and we deliberately added these kinds of things to keep the Dart analyzer useful.

But seriously, you have not explained why you think they're unintuitive; "Peter says so" is not an argument. Can you explain why it's not intuitively obvious that [x] has type [A] or [B] after the if-statement here:

  var x;
  if (c) {
    x = new A();
  } else {
    x = new B();
  }
  // Here [x] has type [A] or [B].

I don't think writing "[A or B]" instead of "[A] or [B]" suddenly makes things unintuitive.

Also, in case you did not read the Facebook JS type system thread, Facebook's JS typs system has union types: https://www.youtube.com/watch?v=Bse0sYR7oVY&t=83m36s So, there's a precedent, for what it's worth.

[munificent]

Facebook's JS typs system has union types: https://www.youtube.com/watch?v=Bse0sYR7oVY&t=83m36s So, there's a precedent, for what it's worth.

Here's some more:

• StrongTalk had union types.
• The Closure Compiler that lots of Google uses to add an optional type system to JS has union types.
• Facebook's Hack language which adds an optional type system to PHP.
• Typed Racket, an optional type system for Scheme.
• mypy, an optional type system for Python that Guido recently took an interest in.
• Julia has them.
• So does Ceylon.
• Pike, another older optionally typed language.
• And, of course, any language with nullable or non-nullable types has at least one limited form of union types.

The only optionally typed languages I know of off-hand that don't have union types are ActionScript, TypeScript, and Dart. TypeScript has a limited form of them by allowing method overloading in interfaces and also leans heavily towards statically typed variables so you don't run into union cases as often from what I gather.

[lukechurch]

@collinsn

I'm not sure what you mean by intuitive in this context, It's a fairly overloaded word, could you give me a little more detail as to what you mean?

[peter-ahe-google]

@collinsn I did not start making claims that union types are a "simple, intuitive concept", you did. It is you that is making unfounded claims, and I'm objecting to that.

I'm not objecting to the analyzer using union types internally. In fact, I've been long arguing for the analyzer needing a more complex inference algorithm, where it can track information that cannot be represented in source code.

However, I also know from previous experience just how much you can confuse users when you expose the internal details of type inference to users. My experience comes from being the javac tech lead at Sun Microsystems just after we shipped JDK 5. That mean that I saw all the incoming language and compiler bugs. I also spoke a conferences, and was involved in various communities. I've also helped a lot of my coworkers around issues in the Java type system. Based on this, I've formed some opinions on what I think is intuitive, and what isn't.

Here are a few guidelines that I think will serve our users:

* Do not expose inferred types that the user haven't written directly.

* Do not expose inferred types that cannot be expressed in the language.

* Don't trust type theoreticians (or Ph.D. students) who claim that a concept is simple. Most likely, they haven't made any studies whatsoever to back their claims. They have probably lost touch with how people outside the field of type theory think, and might have forgotten they aren't targeting people with a degree in CS.

How do I apply these guidelines? Let's examine the message originally reported:

"The argument type '{BadInterfaceType,BadTypedefType,TypedefType,MalformedType,InterfaceType}' cannot be assigned to the parameter type 'GenericType'"

I've looked at the listed types, and the issue is that MalformedType typed isn't a subtype of GenericType. All the other types are. So I claim this would be a better message:

"The expression 'type' might have the type 'MalformedType' which can't be assigned to 'GenericType'."

Then I'd add this additional information about line 2019:

        type = checkNoTypeArguments(type);

"The method 'checkNoTypeArguments' may return a 'MalformedType'."

I'm really surprised that you're arguing that it is a better approach to use abstract concepts that aren't part of the language instead of concrete actionable information like this.

Let's revisit if union types are intuitive, I know they aren't intuitive because they confuse me. They also confuse you:

"The definition of union-type subtyping is now

  {A1, ..., An} <: B

if

  Ai <: B

for any [i]."

I believe this is a type rule for intersection types, and you're now proposing to infer intersection types. I'm not sure that is the right approach.

The members of an intersection type A & B is the union of all the members of A and B. Because only types that implement both A and B are in the set.

The members of an union type A | B is the intersection of all the members of A and B. Because type that implement either A or B are in the set.

And this brings me back to my experience, most times when I hear people talking about union types, they're actually talking about intersection types. So I can object to when you say they're intuitive, and I can make the counterclaim that they aren't. But it is a weird discussion to have. We're not discussing if we should add union types to Dart (even if Bob thinks we are), we're discussing if the messages produced by the analyzer are confusing.

[DartBot]

This comment was originally written by [email protected]

---

My internship ends on Friday and we still haven't agreed on a UI, so I've gone ahead and put the union types behind a flag ([enableUnionTypes]) and disabled them by default. I've also bumped the milestone to 1.8 and changed the owner to @­lukechurch (he had some UI ideas and was interested in doing some experiments).

Instructions for enabling union types are included in the CL description:

https://codereview.chromium.org/592923002/

In another CL, not yet landed, I'm making the semantics of union types controllable by another flag ([strictUnionTypes]). This will help with @­lukechurch's experiments. The default is non-strict / permissive union types, which have intersection-type semantics. The non-strict semantics are more in the spirit of Dart's other "if it might make sense we allow it" rules, e.g. the assignment compatibility rule for interface types:

  A <=> B iff A <: B or B <: A

However, our inference is only sound for the strict semantics. For example

  var x;
  if (c) {
    x = new A();
  } else {
    x = new B();
  }
  // Here [x] has type [A] or [B].

Using the permissive / intersection-type semantics, e.g. saying that methods defined on [A] or on [B] are defined on [x] after the join point is obviously unsound, but we choose this as the default because it minimizes false positives (hints when there is not actually any problem). For example, using the strict / union-type semantics where a method is only defined on [x] if it's defined on both [A] and [B], we get a false positive for code like this:

  class A {
    m() => 0;
  }
  
  class B {}
  
  main() {
    var x;
    if (0 < 1) {
      x = new A();
    } else {
      x = new B();
    }
    if (0 < 1) {
      // Here we get a hint that [m] is not defined on [A or B] when using the
      // strict semantics. We don't get the warning using the permissive
      // semantics, since [m] is defined on [A].
      x.m();
    }
  }

I expect that in the common case the strict semantics are more useful -- and indeed, it's easy enough to refactor the above code to eliminate the warning, by moving the method call into the if-statement -- but the rule for analyzer hints seems to be "thou shalt not generate a false positive", because there's no way to disable a hint.

In a GVC with @­lukechurch and @­brianwilkerson we discussed ways forward, coming away with two plans:

1. compute a proof-tree like object along with the union types, that explains where the union type came from.

Using the proof tree, we can provide a much more helpful message to the user. This should help address @­ahe's concern about saying more clearly what the problem is. This will probably be more useful with the strict semantics. E.g., for the code

   1 class A {
   2 m() => 0;
   3 }
   4
   5 class B {}
   6
   7 main() {
   8 var x;
   9 if (0 < 1) {
  10 x = new A();
  11 } else {
  12 x = new B();
  13 }
  14 // For the strict semantics we rightly complain here that [m] is not
  15 // defined on [A or B].
  16 x.m();
  17 }

we compute a proof tree like

  ----- Assignment line 10 ----- Assignment line 12
  x : A x : B
  --------------------------------- If-statement join point line 13
  x : A or B

and then can give a very helpful hint like

  line 16: the method [m] may not be defined on [x] because [x] may have type [B]
           from the assignment on line 12 and [m] is not defined on [B].

1. run analyzer on various large Dart code bases, using both strict and permissive union types, and see what kind of hints are generated.

Questions this will help answer include "how often are the hints useful?". As mentioned, I'm making the strict vs permissive semantics controllable by a flag, so that it's easy to experiment with both versions of the analysis.

---

Set owner to @lukechurch.
Removed this from the 1.7 milestone.
Added this to the 1.8 milestone.
Added Triaged label.

[DartBot]

This comment was originally written by [email protected]

---

Strict union types internally are here:

https://codereview.chromium.org/599293002

Strict union types externally in the completion UI are next ...

[DartBot]

This comment was originally written by [email protected]

---

Strict union types externally are here:

https://codereview.chromium.org/606753003

[bwilkerson]

Union types were removed a long time ago. I don't believe that this issue is relevant any more.