Least upper bound fixes.

Least upper bound fixes.

Committed: https://code.google.com/p/dart/source/detail?r=28672

[gbracha, 2013-10-14 19:24:04]

I'll send you the PDF for your sanity

[gbracha, 2013-10-15 18:39:59]

Committed patchset #5 manually as r28672 (presubmit successful).

[Johnni Winther, 2013-10-23 07:46:05]

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
File docs/language/dartLangSpec.tex (right):

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5986: where $depth(T)$ is the number of steps in
the longest inheritance path from $T$ to \code{Object}. Let $q$ be the largest
number such that $S_q$ has cardinality one. The least upper bound of $I$ and $J$
is the sole element of  $S_q$.
This part doesn't handle type arguments and therefore fails to ensure the
(natural) invariant: T << S => lub(T, S). For instance lub(List<int>,List<num>)
is Object and not List<num>.

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5988: The least upper bound of \DYNAMIC{} and any
type $T$ is \DYNAMIC{}.
Maybe this should be the opposite to follow the invariant from above.

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5989: The least upper bound of \VOID{} and any
type $T \ne \DYNAMIC{}$ is \VOID{}.
By the definition of << on function types we could say that T << void for any T,
and use the invariant. This would then change lub(void,dynamic) to void which I
think is better anyway. For instance:

void m1() {}
m2() {}

int a = b ? m1() : m2(); // Warning void is not assignable to int.

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5990: Let $U$ be a type variable with upper bound
$B$. The least upper bound of $U$ and a type $T$ is the least upper bound of $B$
and $T$.
This rules follows the invariant!

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5994: % Function types
These rules follows the invariant!

[Johnni Winther, 2013-10-23 12:21:55]

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
File docs/language/dartLangSpec.tex (right):

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5990: Let $U$ be a type variable with upper bound
$B$. The least upper bound of $U$ and a type $T$ is the least upper bound of $B$
and $T$.
Looking closer at this, this is actually not well-defined for the least upper
bound of two type variables. Consider this:

class C<A, B extends A, C extends A, D extends C> {}

Do we have (always try left first)
  lub(B,D) = lub(A,D) = lub(Object,D) = Object
or (always try right first)
  lub(B,D) = lub(B,C) = lub(B,A) = lub(B,Object) = Object
or (use an oracle (try left,right,right,right))
  lub(B,D) = lub(A,D) = lub(A,C) = lub(A,A) = A
or (use another oracle (try right,right,right,left))
  lub(B,D) = lub(B,C) = lub(B,A) = lub(A,A) = A
or (use a dumb oracle (try right,left,left))
  lub(B,D) = lub(B,C) = lub(A,C) = lub(Object,C) = Object
or ... ?

[Johnni Winther, 2013-10-24 11:34:49]

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
File docs/language/dartLangSpec.tex (right):

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5986: where $depth(T)$ is the number of steps in
the longest inheritance path from $T$ to \code{Object}. Let $q$ be the largest
number such that $S_q$ has cardinality one. The least upper bound of $I$ and $J$
is the sole element of  $S_q$.
The missing handling of generic types actually cause a warning in our API. In
the implementation HttpClient we have code like this:

(isSecure ? SecureSocket.connect(...) : Socket.connect(...)).then(...)

Socket.connect returns a Future<Socket> and SecureSocket.connect returns a
Future<SecureSocket> and since the least upper bound is Object we get a warning
on the call to 'then'.

I propose that we either 1) add the invariant rule on the side, i.e. that if T
<< S then lub(T,S) = S, or 2) (the more elaborate) use the algorithm above on
declarations instead of types (finding Future as the most specific common
declaration of Future<Socket> and Future<SecureSocket>) and on each type
variable use the invariant to find the type argument or, if that fails, use
dynamic as type argument (in this case finding Socket as the type argument).

[Johnni Winther, 2013-10-24 14:05:00]

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
File docs/language/dartLangSpec.tex (right):

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5988: The least upper bound of \DYNAMIC{} and any
type $T$ is \DYNAMIC{}.
On 2013/10/23 07:46:05, Johnni Winther wrote:
> Maybe this should be the opposite to follow the invariant from above.

I need to flip a bit in my head: any type _is_ more specific than dynamic! Sorry
for the noise.

https://codereview.chromium.org/27209004/diff/12001/docs/language/dartLangSpe...
docs/language/dartLangSpec.tex:5989: The least upper bound of \VOID{} and any
type $T \ne \DYNAMIC{}$ is \VOID{}.
On 2013/10/23 07:46:05, Johnni Winther wrote:
> By the definition of << on function types we could say that T << void for any
T,
> and use the invariant. This would then change lub(void,dynamic) to void which
I
> think is better anyway. For instance:
> 
> void m1() {}
> m2() {}
> 
> int a = b ? m1() : m2(); // Warning void is not assignable to int.

Again. Noise. (Though a better warning in this example...)