Intersection Types - More Details
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 co- or contravariant type constructor, then C[A] & C[B] can be simplified using the following rules:
- If
Cis covariant,C[A] & C[B] ~> C[A & B] - If
Cis 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 // 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.