[scala] compound types conformance

[Eugene Vigdorchik-2]

When implementing scala plugin for intellij we came across the issue with computing conformance relation between compound types. The spec says that
1) A compound type T1 with . . . with Tn {R } conforms to each of its component
types Ti .
2) If T <:Ui for i = 1, . . . , n and for every binding d of a type or value x in R there
exists a member binding of x in T which subsumes d, then T conforms to the
compound type U1 with . . . with Un {R }.

Clearly case 1 does not apply for computing conformance for 2 compounds. Case 2 does not seem to apply either, since member bindings for compound types do not include structural declarations defined in the type.
Still scalac is able to compare 2 compounds correctly:

scala> class A
defined class A

scala> class B extends A
defined class B

scala> var a : {val v : A} = _
a: AnyRef{def v: A} = null

scala> var b : {val v : B} = _
b: AnyRef{def v: B} = null

scala> a = b
a: AnyRef{def v: A} = null

scala> b = a
<console>:8: error: type mismatch;
 found   : AnyRef{def v: A}
 required: AnyRef{def v: B}
       b = a
           ^

So my question is do I miss something nontrivial in the spec or is this rule indeed missing?

Thank you in advance,
Eugene.

[Geoffrey Alan Washburn-4]

Eugene Vigdorchik wrote:

> When implementing scala plugin for intellij we came across the issue
> with computing conformance relation between compound types. The spec
> says that
> 1) A compound type T1 with . . . with Tn {R } conforms to each of its
> component
> types Ti .
> 2) If T <:Ui for i = 1, . . . , n and for every binding d of a type or
> value x in R there
> exists a member binding of x in T which subsumes d, then T conforms to the
> compound type U1 with . . . with Un {R }.
>
> Clearly case 1 does not apply for computing conformance for 2 compounds.
> Case 2 does not seem to apply either, since member bindings for compound
> types do not include structural declarations defined in the type.
> Still scalac is able to compare 2 compounds correctly:
>
> scala> class A
> defined class A
>
> scala> class B extends A
> defined class B
>
> scala> var a : {val v : A} = _
> a: AnyRef{def v: A} = null
>
> scala> var b : {val v : B} = _
> b: AnyRef{def v: B} = null
>
> scala> a = b
> a: AnyRef{def v: A} = null
>
> scala> b = a
> <console>:8: error: type mismatch;
>  found   : AnyRef{def v: A}
>  required: AnyRef{def v: B}
>        b = a
>            ^
>
> So my question is do I miss something nontrivial in the spec or is this
> rule indeed missing?

Case 2 applies in this instance.  a = b works because b can be promoted
to type { val v : A } because the declaration "val v : B" subsumes the
declaration "val v : A".  b = a doesn't work because there is no way to
promote { val v : B } to have type { val v : A }.

You may just be getting confused because the specification of
conformance is declarative rather than algorithmic.  I would agree that
the wording could maybe be better.  I would have written it as

"If T <:Ui for i = 1, . . . , n and for every declaration d1 in R there
exists a declaration d2 in T which subsumes d1, then T conforms to the
compound type U1 with . . . with Un {R }."

[Martin Odersky]

On Mon, Jul 14, 2008 at 9:52 AM, Eugene Vigdorchik
<eugene.vigdorchik@...> wrote:

> When implementing scala plugin for intellij we came across the issue with
> computing conformance relation between compound types. The spec says that
> 1) A compound type T1 with . . . with Tn {R } conforms to each of its
> component
> types Ti .
> 2) If T <:Ui for i = 1, . . . , n and for every binding d of a type or value
> x in R there
> exists a member binding of x in T which subsumes d, then T conforms to the
> compound type U1 with . . . with Un {R }.
>
> Clearly case 1 does not apply for computing conformance for 2 compounds.
> Case 2 does not seem to apply either, since member bindings for compound
> types do not include structural declarations defined in the type.

Hi Eugene,

The intention is that member bindings for compound types *do* include
structural declarations defined in the type. Is there a part in the
spec that led you to believe otherwise?

Cheers

 -- Martin

[Eugene Vigdorchik-2]

Hello Martin,
I read:
"The member bindings of a type T are all bindings d such that there exists a type
instance of some class C among the base types of T and there exists a definition or
declaration d0 in C such that d results fromd0 by replacing every type T0 in d0 by T0
in C seen from T ."
and:
"The base types of a compound type T1 with . . . with Tn {R } are the reduced
union of the base classes of all Ti 's"
So member bindings for compound type do not include structural declarations according to these definitions?

Eugene.

On Mon, Jul 14, 2008 at 11:31 AM, martin odersky <martin.odersky@...> wrote:

On Mon, Jul 14, 2008 at 9:52 AM, Eugene Vigdorchik
<eugene.vigdorchik@...> wrote:
> When implementing scala plugin for intellij we came across the issue with
> computing conformance relation between compound types. The spec says that
> 1) A compound type T1 with . . . with Tn {R } conforms to each of its
> component
> types Ti .
> 2) If T <:Ui for i = 1, . . . , n and for every binding d of a type or value
> x in R there
> exists a member binding of x in T which subsumes d, then T conforms to the
> compound type U1 with . . . with Un {R }.
>
> Clearly case 1 does not apply for computing conformance for 2 compounds.
> Case 2 does not seem to apply either, since member bindings for compound
> types do not include structural declarations defined in the type.

Hi Eugene,

The intention is that member bindings for compound types *do* include
structural declarations defined in the type. Is there a part in the
spec that led you to believe otherwise?

Cheers

 -- Martin

[Martin Odersky]

Hi Eugene,

You are correct. I have rewritten the para on member bindings as follows:

3. The {\em member bindings} of a type $T$ are (1) all bindings $d$ such that
there exists a type instance of some class $C$ among the base types of $T$
and there exists a definition or declaration $d'$ in $C$
such that $d$ results from $d'$ by replacing every
type $T'$ in $d'$ by $T'$ in $C$ seen from $T$, and (2) all bindings
of the type's refinement (\sref{sec:refinements}), if it has one.

Thanks for pointing out the flaw!

Cheers

 -- Martin