Add spec for intersection types

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.

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)

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
 }