From 693f2e6bdd248e7161372f4d188a3587aa31ecd3 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Wed, 10 Oct 2018 16:11:12 +0200 Subject: [PATCH 1/5] Add spec for intersection types --- .../docs/reference/intersection-types-spec.md | 118 ++++++++++++++++++ docs/docs/reference/intersection-types.md | 41 +----- tests/pos/reference/intersection-types.scala | 43 +++---- 3 files changed, 142 insertions(+), 60 deletions(-) create mode 100644 docs/docs/reference/intersection-types-spec.md diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md new file mode 100644 index 000000000000..74b639bb37e8 --- /dev/null +++ b/docs/docs/reference/intersection-types-spec.md @@ -0,0 +1,118 @@ +--- +layout: doc-page +title: "Intersection Types - More Details" +--- + +## Syntax + +Syntactically, an intersection type is similar to an infix type, +where the infix operator is `&`. + +``` +Type ::= ...| InfixType +InfixType ::= RefinedType {id [nl] RefinedType} +RefinedType ::= WithType {[nl] Refinement} +WithType ::= AnnotType {‘with’ AnnotType} +``` + +## 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 +} +trait Growable[T] { + def add(x: T): this.type +} +def f(x: Resettable & Growable[String]) = { + x.reset() + x.add("first") +} +``` + +The value `x` is required to be _both_ a `Resettable` and a +`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`. + +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 { + def children: List[A] +} +trait B { + def children: List[B] +} +val x: A & B = new C +val ys: List[A & B] = x.children +``` + +The type of `children` in `A & B` is the intersection of `children`'s +type in `A` and its type in `B`, which is `List[A] & List[B]`. This +can be further simplified to `List[A & B]` because `List` is +covariant. + +An intersection type `A & B` may not be inhabited, e.g. `Int & String` is not inhabited. +`A & B` is just a type that represents a set of requirements for +values of the type. At the point where a value is _constructed_, one +must make sure that all inherited members are correctly defined. +So if one defines a class `C` that inherits `A` and `B`, one needs +to give at that point a definition of a `children` method with the required type. + +```scala +class C extends A with B { + def children: List[A & B] = ??? +} +``` + +## 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`. +In another word, `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. + +## 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 +``` + +## 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..82f1572161bf 100644 --- a/docs/docs/reference/intersection-types.md +++ b/docs/docs/reference/intersection-types.md @@ -19,47 +19,10 @@ 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]` 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: - -```scala -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 -``` - -The type of `children` in `A & B` is the intersection of `children`'s -type in `A` and its type in `B`, which is `List[A] & List[B]`. This -can be further simplified to `List[A & B]` because `List` is -covariant. - -One might wonder how the compiler could come up with a definition for -`children` of type `List[A & B]` since all its is given are `children` -definitions of type `List[A]` and `List[B]`. The answer is it does not -need to. `A & B` is just a type that represents a set of requirements for -values of the type. At the point where a value is _constructed_, one -must make sure that all inherited members are correctly defined. -So if one defines a class `C` that inherits `A` and `B`, one needs -to give at that point a definition of a `children` method with the required type. - -```scala -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 } From 2e72550aadecc7c617afd5bb5e2609addbc0dad6 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Wed, 10 Oct 2018 16:24:43 +0200 Subject: [PATCH 2/5] Refine text --- docs/docs/reference/intersection-types-spec.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md index 74b639bb37e8..8f3b54ec28c2 100644 --- a/docs/docs/reference/intersection-types-spec.md +++ b/docs/docs/reference/intersection-types-spec.md @@ -5,7 +5,7 @@ title: "Intersection Types - More Details" ## Syntax -Syntactically, an intersection type is similar to an infix type, +Syntactically, an intersection type `S & T` is similar to an infix type, where the infix operator is `&`. ``` @@ -87,7 +87,7 @@ class C extends A with B { A & B <: T ``` -From the rules above, we can show that `&` is _commutative_: `A & B <: B & A`. +From the rules above, we can show that `&` is _commutative_: `A & B <: B & A` for any type `A` and `B`. In another word, `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. From 2599e2ead09eb84f298f0cdefc0a500ff90d359a Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Oct 2018 17:12:21 +0200 Subject: [PATCH 3/5] Address review --- .../docs/reference/intersection-types-spec.md | 94 +++++++------------ docs/docs/reference/intersection-types.md | 43 ++++++++- 2 files changed, 75 insertions(+), 62 deletions(-) diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md index 8f3b54ec28c2..a7747c0160de 100644 --- a/docs/docs/reference/intersection-types-spec.md +++ b/docs/docs/reference/intersection-types-spec.md @@ -5,70 +5,14 @@ title: "Intersection Types - More Details" ## Syntax -Syntactically, an intersection type `S & T` is similar to an infix type, -where the infix operator is `&`. +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} -RefinedType ::= WithType {[nl] Refinement} -WithType ::= AnnotType {‘with’ AnnotType} -``` - -## 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 -} -trait Growable[T] { - def add(x: T): this.type -} -def f(x: Resettable & Growable[String]) = { - x.reset() - x.add("first") -} -``` - -The value `x` is required to be _both_ a `Resettable` and a -`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`. - -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 { - def children: List[A] -} -trait B { - def children: List[B] -} -val x: A & B = new C -val ys: List[A & B] = x.children -``` - -The type of `children` in `A & B` is the intersection of `children`'s -type in `A` and its type in `B`, which is `List[A] & List[B]`. This -can be further simplified to `List[A & B]` because `List` is -covariant. - -An intersection type `A & B` may not be inhabited, e.g. `Int & String` is not inhabited. -`A & B` is just a type that represents a set of requirements for -values of the type. At the point where a value is _constructed_, one -must make sure that all inherited members are correctly defined. -So if one defines a class `C` that inherits `A` and `B`, one needs -to give at that point a definition of a `children` method with the required type. - -```scala -class C extends A with B { - def children: List[A & B] = ??? -} ``` ## Subtyping Rules @@ -91,6 +35,36 @@ From the rules above, we can show that `&` is _commutative_: `A & B <: B & A` fo In another word, `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 `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 diff --git a/docs/docs/reference/intersection-types.md b/docs/docs/reference/intersection-types.md index 82f1572161bf..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 @@ -21,8 +25,43 @@ def f(x: Resettable & Growable[String]) = { The value `x` is required to be _both_ a `Resettable` and a `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`. +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 { + def children: List[A] +} +trait B { + def children: List[B] +} +val x: A & B = new C +val ys: List[A & B] = x.children +``` + +The type of `children` in `A & B` is the intersection of `children`'s +type in `A` and its type in `B`, which is `List[A] & List[B]`. This +can be further simplified to `List[A & B]` because `List` is +covariant. + +One might wonder how the compiler could come up with a definition for +`children` of type `List[A & B]` since all its is given are `children` +definitions of type `List[A]` and `List[B]`. The answer is it does not +need to. `A & B` is just a type that represents a set of requirements for +values of the type. At the point where a value is _constructed_, one +must make sure that all inherited members are correctly defined. +So if one defines a class `C` that inherits `A` and `B`, one needs +to give at that point a definition of a `children` method with the required type. + +```scala +class C extends A with B { + def children: List[A & B] = ??? +} +``` + + [More details](./type-lambdas-spec.html) From 7e9f3137d938ec082b731df9dbb052c795c97581 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Oct 2018 17:16:35 +0200 Subject: [PATCH 4/5] Add explanation to pseudocode --- .../docs/reference/intersection-types-spec.md | 50 ++++++++++++------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md index a7747c0160de..2bdb51357244 100644 --- a/docs/docs/reference/intersection-types-spec.md +++ b/docs/docs/reference/intersection-types-spec.md @@ -7,8 +7,8 @@ title: "Intersection Types - More Details" 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 &. +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 @@ -18,20 +18,29 @@ InfixType ::= RefinedType {id [nl] RefinedType} ## Subtyping Rules ``` - T <: A T <: B - ---------------- - T <: A & B +T <: A T <: B +---------------- + T <: A & B - A <: T - ---------------- - A & B <: T + A <: T +---------------- + A & B <: T - B <: 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 that sense that the two types have the same values and are subtypes of each other. @@ -74,16 +83,19 @@ 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 +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, we use `|T|` to mean the erased type of `T`, `JArray` means +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 From 4d6aa110e8dd78d8bece2cb2b6e90f955dbd2127 Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Mon, 15 Oct 2018 11:05:02 +0200 Subject: [PATCH 5/5] Small grammatical fixes --- docs/docs/reference/intersection-types-spec.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/docs/reference/intersection-types-spec.md b/docs/docs/reference/intersection-types-spec.md index 2bdb51357244..e7c3d898757b 100644 --- a/docs/docs/reference/intersection-types-spec.md +++ b/docs/docs/reference/intersection-types-spec.md @@ -41,7 +41,7 @@ A & B <: B A & B <: A A & B <: B & A ``` -In another word, `A & B` is the same type as `B & A`, in that sense that the two types +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 @@ -93,7 +93,7 @@ glb(_, B) = B if B is not a trait glb(A, _) = A ``` -In the above, we use `|T|` to mean the erased type of `T`, `JArray` means +In the above, `|T|` means the erased type of `T`, `JArray` refers to the type of Java Array. ## Relationship with Compound Type (`with`)