Intersection type
Type systems 

General concepts 
Major categories 

Minor categories 
See also 
In type theory, an intersection type can be allocated to values that can be assigned both the type [math]\displaystyle{ \sigma }[/math] and the type [math]\displaystyle{ \tau }[/math]. This value can be given the intersection type [math]\displaystyle{ \sigma \cap \tau }[/math] in an intersection type system.^{[1]}
Generally, if the ranges of values of two types overlap, then a value belonging to the intersection of the two ranges can be assigned the intersection type of these two types. Such a value can be safely passed as argument to functions expecting either of the two types.
For example, in Java the class Boolean
implements both the Serializable
and the Comparable
interfaces. Therefore, an object of type Boolean
can be safely passed to functions expecting an argument of type Serializable
and to functions expecting an argument of type Comparable
.
Intersection types are composite data types. Similar to product types, they are used to assign several types to an object. However, product types are assigned to tuples, so that each tuple element is assigned a particular product type component. In comparison, underlying objects of intersection types are not necessarily composite. A restricted form of intersection types are refinement types.
Intersection types are useful for describing overloaded functions.^{[2]} For example, if Template:TSlang is the type of function taking a number as an argument and returning a number, and Template:TSlang is the type of function taking a string as an argument and returning a string, then the intersection of these two types can be used to describe (overloaded) functions that do one or the other, based on what type of input they are given.
Contemporary programming languages, including Ceylon, Flow, Java, Scala, TypeScript, and Whiley (see comparison of languages with intersection types), use intersection types to combine interface specifications and to express ad hoc polymorphism. Complementing parametric polymorphism, intersection types may be used to avoid class hierarchy pollution from crosscutting concerns and reduce boilerplate code, as shown in the TypeScript example below.
The type theoretic study of intersection types is referred to as the intersection type discipline.^{[3]} Remarkably, program termination can be precisely characterized using intersection types.^{[4]}
TypeScript example
TypeScript supports intersection types,^{[5]} improving expressiveness of the type system and reducing potential class hierarchy size, demonstrated as follows.
The following program code defines the classes Template:TSlang, Template:TSlang, and Template:TSlang that each have a method Template:TSlang returning an object of either type Template:TSlang, Template:TSlang, or Template:TSlang. Additionally, the functions Template:TSlang and Template:TSlang require arguments of type Template:TSlang and Template:TSlang, respectively.
class Egg { private kind: "Egg" } class Milk { private kind: "Milk" } //produces eggs class Chicken { produce() { return new Egg(); } } //produces milk class Cow { produce() { return new Milk(); } } //produces a random number class RandomNumberGenerator { produce() { return Math.random(); } } //requires an egg function eatEgg(egg: Egg) { return "I ate an egg."; } //requires milk function drinkMilk(milk: Milk) { return "I drank some milk."; }
The following program code defines the ad hoc polymorphic function Template:TSlang that invokes the member function Template:TSlang of the given object Template:TSlang. The function Template:TSlang has two type annotations, namely Template:TSlang and Template:TSlang, connected via the intersection type constructor Template:TSlang. Specifically, Template:TSlang when applied to an argument of type Template:TSlang returns an object of type type Template:TSlang, and when applied to an argument of type Template:TSlang returns an object of type type Template:TSlang. Ideally, Template:TSlang should not be applicable to any object having (possibly by chance) a Template:TSlang method.
//given a chicken, produces an egg; given a cow, produces milk let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) = function (animal: any) { return animal.produce(); };
Finally, the following program code demonstrates type safe use of the above definitions.
var chicken = new Chicken(); var cow = new Cow(); var randomNumberGenerator = new RandomNumberGenerator(); console.log(chicken.produce()); //Egg { } console.log(cow.produce()); //Milk { } console.log(randomNumberGenerator.produce()); //0.2626353555444987 console.log(animalToFood(chicken)); //Egg { } console.log(animalToFood(cow)); //Milk { } //console.log(animalToFood(randomNumberGenerator)); //ERROR: Argument of type 'RandomNumberGenerator' is not assignable to parameter of type 'Cow' console.log(eatEgg(animalToFood(chicken))); //I ate an egg. //console.log(eatEgg(animalToFood(cow))); //ERROR: Argument of type 'Milk' is not assignable to parameter of type 'Egg' console.log(drinkMilk(animalToFood(cow))); //I drank some milk. //console.log(drinkMilk(animalToFood(chicken))); //ERROR: Argument of type 'Egg' is not assignable to parameter of type 'Milk'
The above program code has the following properties:
 Lines 1–3 create objects Template:TSlang, Template:TSlang, and Template:TSlang of their respective type.
 Lines 5–7 print for the previously created objects the respective results (provided as comments) when invoking Template:TSlang.
 Line 9 (resp. 10) demonstrates type safe use of the method Template:TSlang applied to Template:TSlang (resp. Template:TSlang).
 Line 11, if uncommented, would result in a type error at compile time. Although the implementation of Template:TSlang could invoke the Template:TSlang method of Template:TSlang, the type annotation of Template:TSlang disallows it. This is in accordance with the intended meaning of Template:TSlang.
 Line 13 (resp. 15) demonstrates that applying Template:TSlang to Template:TSlang (resp. Template:TSlang) results in an object of type Template:TSlang (resp. Template:TSlang).
 Line 14 (resp. 16) demonstrates that applying Template:TSlang to Template:TSlang (resp. Template:TSlang) does not result in an object of type Template:TSlang (resp. Template:TSlang). Therefore, if uncommented, line 14 (resp. 16) would result in a type error at compile time.
Comparison to inheritance
The above minimalist example can be realized using inheritance, for instance by deriving the classes Template:TSlang and Template:TSlang from a base class Template:TSlang. However, in a larger setting, this could be disadvantageous. Introducing new classes into a class hierarchy is not necessarily justified for crosscutting concerns, or maybe outright impossible, for example when using an external library. Imaginably, the above example could be extended with the following classes:
 a class Template:TSlang that does not have a Template:TSlang method;
 a class Template:TSlang that has a Template:TSlang method returning Template:TSlang;
 a class Template:TSlang that has a Template:TSlang method, which can be used only once, returning Template:TSlang.
This may require additional classes (or interfaces) specifying whether a produce method is available, whether the produce method returns food, and whether the produce method can be used repeatedly. Overall, this may pollute the class hierarchy.
Comparison to duck typing
The above minimalist example already shows that duck typing is less suited to realize the given scenario. While the class Template:TSlang contains a Template:TSlang method, the object Template:TSlang should not be a valid argument for Template:TSlang. The above example can be realized using duck typing, for instance by introducing a new field Template:TSlang to the classes Template:TSlang and Template:TSlang signifying that objects of corresponding type are valid arguments for Template:TSlang. However, this would not only increase the size of the respective classes (especially with the introduction of more methods similar to Template:TSlang), but is also a nonlocal approach with respect to Template:TSlang.
Comparison to function overloading
The above example can be realized using function overloading, for instance by implementing two methods Template:TSlang and Template:TSlang. In TypeScript, such a solution is almost identical to the provided example. Other programming languages, such as Java, require distinct implementations of the overloaded method. This may lead to either code duplication or boilerplate code.
Comparison to the visitor pattern
The above example can be realized using the visitor pattern. It would require each animal class to implement an Template:TSlang method accepting an object implementing the interface Template:TSlang (adding nonlocal boilerplate code). The function Template:TSlang would be realized as the Template:TSlang method of an implementation of Template:TSlang. Unfortunately, the connection between the input type (Template:TSlang or Template:TSlang) and the result type (Template:TSlang or Template:TSlang) would be difficult to represent.
Limitations
On the one hand, intersection types can be used to locally annotate different types to a function without introducing new classes (or interfaces) to the class hierarchy. On the other hand, this approach requires all possible argument types and result types to be specified explicitly. If the behavior of a function can be specified precisely by either a unified interface, parametric polymorphism, or duck typing, then the verbose nature of intersection types is unfavorable. Therefore, intersection types should be considered complementary to existing specification methods.
Dependent intersection type
A dependent intersection type, denoted [math]\displaystyle{ (x : \sigma) \cap \tau }[/math], is a dependent type in which the type [math]\displaystyle{ \tau }[/math] may depend on the term variable [math]\displaystyle{ x }[/math].^{[6]} In particular, if a term [math]\displaystyle{ M }[/math] has the dependent intersection type [math]\displaystyle{ (x : \sigma) \cap \tau }[/math], then the term [math]\displaystyle{ M }[/math] has both the type [math]\displaystyle{ \sigma }[/math] and the type [math]\displaystyle{ \tau[x := M] }[/math], where [math]\displaystyle{ \tau[x := M] }[/math] is the type which results from replacing all occurrences of the term variable [math]\displaystyle{ x }[/math] in [math]\displaystyle{ \tau }[/math] by the term [math]\displaystyle{ M }[/math].
Scala example
Scala supports type declarations ^{[7]} as object members. This allows a type of an object member to depend on the value of another member, which is called a pathdependent type.^{[8]}
For example, the following program text defines a Scala trait Witness
, which can be used to implement the singleton pattern.^{[9]}
trait Witness { type T val value: T {} }
The above trait Witness
declares the member T
, which can be assigned a type as its value, and the member value
, which can be assigned a value of type T
.
The following program text defines an object booleanWitness
as instance of the above trait Witness
.
The object booleanWitness
defines the type T
as Boolean
and the value value
as true
.
For example, executing System.out.println(booleanWitness.value)
prints true
on the console.
object booleanWitness extends Witness { type T = Boolean val value = true }
Let [math]\displaystyle{ \langle \textsf{x} : \sigma \rangle }[/math] be the type (specifically, a record type) of objects having the member [math]\displaystyle{ \textsf{x} }[/math] of type [math]\displaystyle{ \sigma }[/math].
In the above example, the object booleanWitness
can be assigned the dependent intersection type [math]\displaystyle{ (x : \langle \textsf{T} : \text{Type} \rangle) \cap \langle \textsf{value} : x.\textsf{T} \rangle }[/math].
The reasoning is as follows. The object booleanWitness
has the member T
that is assigned the type Boolean
as its value.
Since Boolean
is a type, the object booleanWitness
has the type [math]\displaystyle{ \langle \textsf{T} : \text{Type} \rangle }[/math].
Additionally, the object booleanWitness
has the member value
that is assigned the value true
of type Boolean
.
Since the value of booleanWitness.T
is Boolean
, the object booleanWitness
has the type [math]\displaystyle{ \langle \textsf{value} : \textsf{booleanWitness.T} \rangle }[/math].
Overall, the object booleanWitness
has the intersection type [math]\displaystyle{ \langle \textsf{T} : \text{Type} \rangle \cap \langle \textsf{value} : \textsf{booleanWitness.T} \rangle }[/math].
Therefore, presenting selfreference as dependency, the object booleanWitness
has the dependent intersection type [math]\displaystyle{ (x : \langle \textsf{T} : \text{Type} \rangle) \cap \langle \textsf{value} : x.\textsf{T} \rangle }[/math].
Alternatively, the above minimalistic example can be described using dependent record types.^{[10]} In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept.^{[6]}
Intersection of a type family
An intersection of a type family, denoted [math]\displaystyle{ \bigcap_{x : \sigma} \tau }[/math], is a dependent type in which the type [math]\displaystyle{ \tau }[/math] may depend on the term variable [math]\displaystyle{ x }[/math]. In particular, if a term [math]\displaystyle{ M }[/math] has the type [math]\displaystyle{ \bigcap_{x : \sigma} \tau }[/math], then for each term [math]\displaystyle{ N }[/math] of type [math]\displaystyle{ \sigma }[/math], the term [math]\displaystyle{ M }[/math] has the type [math]\displaystyle{ \tau[x := N] }[/math]. This notion is also called implicit Pi type,^{[11]} observing that the argument [math]\displaystyle{ N }[/math] is not kept at term level.
Comparison of languages with intersection types
Language  Actively developed  Paradigm(s)  Status  Features 

C#  Yes^{[12]}  Under discussion^{[13]}  Additionally, generic type parameters can have constraints that require their (monomorphized) typearguments to implement multiple interfaces, whereupon the runtime type represented by the generic type parameter becomes an intersectiontype of all listed interfaces.  
Ceylon  Yes^{[14]}  Supported^{[15]} 
 
F#  Yes^{[16]}  Under discussion^{[17]}  ?  
Flow  Yes^{[18]}  Supported^{[19]} 
 
Forsythe  No  Supported^{[20]} 
 
Java  Yes^{[21]}  Supported^{[22]} 
 
PHP  Yes^{[23]}  Supported^{[24]} 
 
Scala  Yes^{[25]}  Supported^{[26]}^{[27]} 
 
TypeScript  Yes^{[28]}  Supported^{[5]} 
 
Whiley  Yes^{[29]}  Supported^{[30]}  ? 
References
 ↑ Barendregt, Henk; Coppo, Mario; DezaniCiancaglini, Mariangiola (1983). "A filter lambda model and the completeness of type assignment". Journal of Symbolic Logic 48 (4): 931–940. doi:10.2307/2273659.
 ↑ Palsberg, Jens (2012). "Overloading is NPComplete". Logic and Program Semantics. Lecture Notes in Computer Science. 7230. pp. 204–218. doi:10.1007/9783642294853_13. ISBN 9783642294846.
 ↑ Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013). Lambda Calculus with Types. Cambridge University Press. pp. 1–. ISBN 9780521766142. https://books.google.com/books?id=2UVasvrhXl8C&pg=PR1.
 ↑ Ghilezan, Silvia (1996). "Strong normalization and typability with intersection types". Notre Dame Journal of Formal Logic 37 (1): 44–52. doi:10.1305/ndjfl/1040067315.
 ↑ ^{5.0} ^{5.1} "Intersection Types in TypeScript". https://www.typescriptlang.org/docs/handbook/advancedtypes.html#intersectiontypes.
 ↑ ^{6.0} ^{6.1} Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". LICS 2003. IEEE Computer Society. pp. 86–95. doi:10.1109/LICS.2003.1210048.
 ↑ "Type declarations in Scala". https://www.scalalang.org/files/archive/spec/2.12/04basicdeclarationsanddefinitions.html#typedeclarationsandtypealiases.
 ↑ Amin, Nada; Grütter, Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro (2016). "The essence of dependent object types". Lecture Notes in Computer Science. A List of Successes That Can Change the World  Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Springer) 9600: 249–272. doi:10.1007/9783319309361_14. ISBN 9783319309354. https://infoscience.epfl.ch/record/215280/files/paper_1.pdf.
 ↑ "Singletons in the Scala shapeless library". https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/singletons.scala.
 ↑ Pollack, Robert (2000). "Dependently typed records for representing mathematical structure". TPHOLs 2000. Springer. pp. 462–479. doi:10.1007/3540446591_29.
 ↑ Stump, Aaron (2018). "From realizability to induction via dependent intersection". Annals of Pure and Applied Logic 169 (7): 637–655. doi:10.1016/j.apal.2018.03.002.
 ↑ "C# Guide". http://csharp.net/.
 ↑ "Discussion: Union and Intersection types in C Sharp". https://github.com/dotnet/csharplang/issues/399.
 ↑ "Eclipse Ceylon: Welcom to Ceylon". https://ceylonlang.org/.
 ↑ "Intersection Types in Ceylon". https://ceylonlang.org/documentation/tour/types/#intersection_types.
 ↑ "F# Software Foundation". http://fsharp.org/.
 ↑ "Add Intersection Types to F Sharp". https://github.com/fsharp/fslangsuggestions/issues/600.
 ↑ "Flow: A Static Type Checker for JavaScript". https://flow.org/en/.
 ↑ "Intersection Type Syntax in Flow". https://flow.org/en/docs/types/intersections/#intersectiontypesyntax.
 ↑ Reynolds, J. C. (1988). Preliminary design of the programming language Forsythe.
 ↑ "Java Software". https://www.oracle.com/java/.
 ↑ "IntersectionType (Java SE 12 & JDK 12)". https://docs.oracle.com/en/java/javase/12/docs/api/java.compiler/javax/lang/model/type/IntersectionType.html.
 ↑ "php.net". https://php.net.
 ↑ "PHP.Watch  PHP 8.1: Intersection Types". https://php.watch/versions/8.1/intersectiontypes.
 ↑ "The Scala Programming Language". https://scalalang.org/.
 ↑ "Compound Types in Scala". https://www.scalalang.org/files/archive/spec/2.12/03types.html#compoundtypes.
 ↑ "Intersection Types in Dotty". http://dotty.epfl.ch/docs/reference/newtypes/intersectiontypes.html.
 ↑ "TypeScript  JavaScript that scales.". https://www.typescriptlang.org/.
 ↑ "Whiley: an Open Source Programming Language with Extended Static Checking". http://whiley.org/.
 ↑ "Whiley language specification". http://whiley.org/download/WhileyLanguageSpec.pdf.
Original source: https://en.wikipedia.org/wiki/Intersection type.
Read more 