diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md new file mode 100644 index 000000000000..e7c3d898757b --- /dev/null +++ b/docs/docs/reference/intersection-types-spec.md @@ -0,0 +1,104 @@ +--- +layout: doc-page +title: "Intersection Types - More Details" +--- + +## Syntax + +Syntactically, an intersection type `S & T` is similar to an infix type, where +the infix operator is `&`. `&` is treated as a soft keyword. That is, it is a +normal identifier with the usual precedence. But a type of the form `A & B` is +always recognized as an intersection type, without trying to resolve `&`. + +``` +Type ::= ...| InfixType +InfixType ::= RefinedType {id [nl] RefinedType} +``` + +## Subtyping Rules + +``` +T <: A T <: B +---------------- + T <: A & B + + A <: T +---------------- + A & B <: T + + B <: T +---------------- + A & B <: T +``` + +From the rules above, we can show that `&` is _commutative_: `A & B <: B & A` for any type `A` and `B`. + +``` + B <: B A <: A +---------- ----------- +A & B <: B A & B <: A +--------------------------- + A & B <: B & A +``` + +In another word, `A & B` is the same type as `B & A`, in the sense that the two types +have the same values and are subtypes of each other. + +If `C` is a type constructor, the join `C[A] & C[B]` is simplified by pulling the +intersection inside the constructor, using the following two rules: + +- If `C` is covariant, `C[A] & C[B] ~> C[A & B]` +- If `C` is contravariant, `C[A] & C[B] ~> C[A | B]` + +When `C` is covariant, `C[A & B] <: C[A] & C[B]` can be derived: + +``` + A <: A B <: B + ---------- --------- + A & B <: A A & B < B +--------------- ----------------- +C[A & B] <: C[A] C[A & B] <: C[B] +------------------------------------------ + C[A & B] <: C[A] & C[B] +``` + +When `C` is contravariant, `C[A | B] <: C[A] & C[B]` can be derived: + +``` + A <: A B <: B + ---------- --------- + A <: A | B B < A | B +------------------- ---------------- +C[A | B] <: C[A] C[A | B] <: C[B] +-------------------------------------------------- + C[A | B] <: C[A] & C[B] +``` + +## Erasure + +The erased type for `S & T` is the erased _glb_ (greatest lower bound) of the +erased type of `S` and `T`. The rules for erasure of intersection types are given +below in pseudocode: + +``` +|S & T| = glb(|S|, |T|) + +glb(JArray(A), JArray(B)) = JArray(glb(A, B)) +glb(JArray(T), _) = JArray(T) +glb(_, JArray(T)) = JArray(T) +glb(A, B) = A if A extends B +glb(A, B) = B if B extends A +glb(A, _) = A if A is not a trait +glb(_, B) = B if B is not a trait +glb(A, _) = A +``` + +In the above, `|T|` means the erased type of `T`, `JArray` refers to +the type of Java Array. + +## Relationship with Compound Type (`with`) + +Intersection types `A & B` replace compound types `A with B` in Scala 2. For the +moment, the syntax `A with B` is still allowed and interpreted as `A & B`, but +its usage as a type (as opposed to in a `new` or `extends` clause) will be +deprecated and removed in the future. diff --git a/docs/docs/reference/intersection-types.md b/docs/docs/reference/intersection-types.md index 3e3ec3d9941b..4e27fd6c5c48 100644 --- a/docs/docs/reference/intersection-types.md +++ b/docs/docs/reference/intersection-types.md @@ -5,6 +5,10 @@ title: "Intersection Types" Used on types, the `&` operator creates an intersection type. +## Type Checking + +The type `S & T` represents values that are of the type `S` and `T` at the same time. + ```scala trait Resettable { def reset(): this.type @@ -19,19 +23,14 @@ def f(x: Resettable & Growable[String]) = { ``` The value `x` is required to be _both_ a `Resettable` and a -`Growable[String]`. Intersection types `A & B` replace compound types -`A with B` in Scala 2. For the moment, `A with B` is still allowed, but -its usage as a type (as opposed to in a `new` or `extends` clause) will be deprecated and removed in the future. +`Growable[String]`. -The members of an intersection type `A & B` are all the members of `A` -and all the members of `B`. For instance `Resettable & Growable[String]` +The members of an intersection type `A & B` are all the members of `A` and all +the members of `B`. For instance `Resettable & Growable[String]` has member methods `reset` and `add`. -`&` is _commutative_: `A & B` is the same type as `B & A`, in that sense that the two types -have the same values and are subtypes of each other. - -If a member appears in both `A` and `B`, its type in `A & B` is the -intersection of its type in `A` and its type in `B`. For instance, assume the definitions: +If a member appears in both `A` and `B`, its type in `A & B` is the intersection +of its type in `A` and its type in `B`. For instance, assume the definitions: ```scala trait A { @@ -63,3 +62,6 @@ class C extends A with B { def children: List[A & B] = ??? } ``` + + +[More details](./type-lambdas-spec.html) diff --git a/tests/pos/reference/intersection-types.scala b/tests/pos/reference/intersection-types.scala index 1d6a14ffa3b1..b36f52028739 100644 --- a/tests/pos/reference/intersection-types.scala +++ b/tests/pos/reference/intersection-types.scala @@ -1,35 +1,36 @@ package intersectionTypes object t1 { + trait Resetable { + def reset(): this.type + } -trait Resetable { - def reset(): this.type -} -trait Growable[T] { - def add(x: T): this.type -} -def f(x: Resetable & Growable[String]) = { - x.reset() - x.add("first") -} + trait Growable[T] { + def add(x: T): this.type + } + def f(x: Resetable & Growable[String]) = { + x.reset() + x.add("first") + } } object t2 { -trait A { - def children: List[A] -} -trait B { - def children: List[B] -} -val x: A & B = new C -val ys: List[A & B] = x.children + trait A { + def children: List[A] + } + trait B { + def children: List[B] + } -class C extends A with B { - def children: List[A & B] = ??? -} + val x: A & B = new C + val ys: List[A & B] = x.children + class C extends A with B { + def children: List[A & B] = ??? + } + val z: B & A = x // commutative }