Intersection Types - More Details

Edit this page on GitHub

Syntax

Syntactically, the type S & T is an infix type, where the infix operator is &. The operator & is a normal identifier with the usual precedence and subject to usual resolving rules. Unless shadowed by another definition, it resolves to the type scala.&, which acts as a type alias to an internal representation of intersection types.

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:

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                     // use first

In the above, |T| means the erased type of T, JArray refers to the type of Java Array.

See also: TypeErasure#erasedGlb

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.