View source for Intersection type

{{short description|Concept in type theory}}
{{Type systems}}
In [[Type theory|type theory]], an '''intersection type''' can be allocated to values that can be assigned both the type <math>\sigma</math> and the type <math>\tau</math>. This value can be given the intersection type <math>\sigma \cap \tau</math> in an intersection type system.<ref name=BCD83>{{cite journal |doi=10.2307/2273659 |jstor=2273659 |title=A filter lambda model and the completeness of type assignment |journal=Journal of Symbolic Logic |volume=48 |issue=4 |pages=931–940 |year=1983 |last1=Barendregt |first1=Henk |last2=Coppo |first2=Mario |last3=Dezani-Ciancaglini |first3=Mariangiola|s2cid=45660117 |}}</ref>
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 (programming language)|Java]] the class {{code|Boolean}} implements both the {{code|Serializable}} and the {{code|Comparable}} interfaces. Therefore, an object of type {{code|Boolean}} can be safely passed to functions expecting an argument of type {{code|Serializable}} and to functions expecting an argument of type {{code|Comparable}}.

Intersection types are [[Composite data type|composite data type]]s. Similar to [[Product type|product type]]s, they are used to assign several types to an object.
However, product types are assigned to [[Tuple|tuple]]s, 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 type|refinement type]]s.

Intersection types are useful for describing overloaded functions.<ref>{{cite book |doi=10.1007/978-3-642-29485-3_13 |chapter=Overloading is NP-Complete |title=Logic and Program Semantics |volume=7230 |pages=204–218 |series=Lecture Notes in Computer Science |year=2012 |last1=Palsberg |first1=Jens |isbn=978-3-642-29484-6 }}</ref> For example, if {{TS-lang|1=number => number}} is the type of function taking a number as an argument and returning a number, and {{TS-lang|1=string => string}} 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 (programming language)|Ceylon]], Flow, [[Java (programming language)|Java]], [[Scala (programming language)|Scala]], TypeScript, and [[Whiley (programming language)|Whiley]] (see comparison of languages with intersection types), use intersection types to combine interface specifications and to express [[Ad hoc polymorphism|ad hoc polymorphism]].
Complementing [[Parametric polymorphism|parametric polymorphism]], intersection types may be used to avoid class hierarchy pollution from [[Cross-cutting concern|cross-cutting concern]]s and reduce [[Boilerplate code|boilerplate code]], as shown in the TypeScript example below.

The [[Type theory|type theoretic]] study of intersection types is referred to as the [[Intersection type discipline|intersection type discipline]].<ref>{{cite book|author1=Henk Barendregt|author2=Wil Dekkers|author3=Richard Statman|title=Lambda Calculus with Types|url=https://books.google.com/books?id=2UVasvrhXl8C&pg=PR1|date=20 June 2013|publisher=Cambridge University Press|isbn=978-0-521-76614-2|pages=1–}}</ref>
Remarkably, program termination can be precisely characterized using intersection types.<ref name=G96>{{cite journal |doi=10.1305/ndjfl/1040067315 |title=Strong normalization and typability with intersection types |journal=Notre Dame Journal of Formal Logic |volume=37 |issue=1 |pages=44–52 |year=1996 |last1=Ghilezan |first1=Silvia |doi-access=free }}</ref>

== TypeScript example ==
[[TypeScript]] supports intersection types,<ref name=TS/> improving expressiveness of the type system and reducing potential class hierarchy size, demonstrated as follows.

The following program code defines the classes {{TS-lang|Chicken}}, {{TS-lang|Cow}}, and {{TS-lang|RandomNumberGenerator}} that each have a method {{TS-lang|produce}} returning an object of either type {{TS-lang|Egg}}, {{TS-lang|Milk}}, or {{TS-lang|number}}.
Additionally, the functions {{TS-lang|eatEgg}} and {{TS-lang|drinkMilk}} require arguments of type {{TS-lang|Egg}} and {{TS-lang|Milk}}, respectively.

<source lang="typescript">
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.";
}
</source>

The following program code defines the [[Ad hoc polymorphism|ad hoc polymorphic]] function {{TS-lang|animalToFood}} that invokes the member function {{TS-lang|produce}} of the given object {{TS-lang|animal}}.
The function {{TS-lang|animalToFood}} has ''two'' type annotations, namely {{TS-lang|1=((_: Chicken) => Egg)}} and {{TS-lang|1=((_: Cow) => Milk)}}, connected via the intersection type constructor {{TS-lang|1=&}}.
Specifically, {{TS-lang|animalToFood}} when applied to an argument of type {{TS-lang|Chicken}} returns an object of type type {{TS-lang|Egg}}, and when applied to an argument of type {{TS-lang|Cow}} returns an object of type type {{TS-lang|Milk}}.
Ideally, {{TS-lang|animalToFood}} should not be applicable to any object having (possibly by chance) a {{TS-lang|produce}} method.
<source lang="typescript">
// given a chicken, produces an egg; given a cow, produces milk
let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) =
    function (animal: any) {
        return animal.produce();
    };
</source>

Finally, the following program code demonstrates [[Type safety|type safe]] use of the above definitions. 
<source lang="typescript" line>
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'
</source>
The above program code has the following properties:
* Lines 1–3 create objects {{TS-lang|chicken}}, {{TS-lang|cow}}, and {{TS-lang|randomNumberGenerator}} of their respective type.
* Lines 5–7 print for the previously created objects the respective results (provided as comments) when invoking {{TS-lang|produce}}.
* Line 9 (resp. 10) demonstrates type safe use of the method {{TS-lang|animalToFood}} applied to {{TS-lang|chicken}} (resp. {{TS-lang|cow}}).
* Line 11, if uncommented, would result in a type error at compile time. Although the ''implementation'' of {{TS-lang|animalToFood}} could invoke the {{TS-lang|produce}} method of {{TS-lang|randomNumberGenerator}}, the ''type annotation'' of {{TS-lang|animalToFood}} disallows it. This is in accordance with the intended meaning of {{TS-lang|animalToFood}}.
* Line 13 (resp. 15) demonstrates that applying {{TS-lang|animalToFood}} to {{TS-lang|chicken}} (resp. {{TS-lang|cow}}) results in an object of type {{TS-lang|Egg}} (resp. {{TS-lang|Milk}}).
* Line 14 (resp. 16) demonstrates that applying {{TS-lang|animalToFood}} to {{TS-lang|cow}} (resp. {{TS-lang|chicken}}) does not result in an object of type {{TS-lang|Egg}} (resp. {{TS-lang|Milk}}). 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 (object-oriented programming)|inheritance]], for instance by deriving the classes {{TS-lang|Chicken}} and {{TS-lang|Cow}} from a base class {{TS-lang|Animal}}.
However, in a larger setting, this could be disadvantageous.
Introducing new classes into a class hierarchy is not necessarily justified for [[Cross-cutting concern|cross-cutting concern]]s, or maybe outright impossible, for example when using an external library. 
Imaginably, the above example could be extended with the following classes:
* a class {{TS-lang|Horse}} that does not have a {{TS-lang|produce}} method;
* a class {{TS-lang|Sheep}} that has a {{TS-lang|produce}} method returning {{TS-lang|Wool}};
* a class {{TS-lang|Pig}} that has a {{TS-lang|produce}} method, which can be used only once, returning {{TS-lang|Meat}}.
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|duck typing]] is less suited to realize the given scenario.
While the class {{TS-lang|RandomNumberGenerator}} contains a {{TS-lang|produce}} method, the object {{TS-lang|randomNumberGenerator}} should not be a valid argument for {{TS-lang|animalToFood}}.
The above example can be realized using duck typing, for instance by introducing a new field {{TS-lang|argumentForAnimalToFood}} to the classes {{TS-lang|Chicken}} and {{TS-lang|Cow}} signifying that objects of corresponding type are valid arguments for {{TS-lang|animalToFood}}.
However, this would not only increase the size of the respective classes (especially with the introduction of more methods similar to {{TS-lang|animalToFood}}), but is also a non-local approach with respect to {{TS-lang|animalToFood}}.

=== Comparison to function overloading ===
The above example can be realized using function overloading, for instance by implementing two methods {{TS-lang|animalToFood(animal: Chicken): Egg}} and {{TS-lang|animalToFood(animal: Cow): Milk}}.
In TypeScript, such a solution is almost identical to the provided example. 
Other programming languages, such as [[Java (programming language)|Java]], require distinct implementations of the overloaded method.
This may lead to either code duplication or [[Boilerplate code|boilerplate code]].

=== Comparison to the visitor pattern ===
The above example can be realized using the [[Visitor pattern|visitor pattern]].
It would require each animal class to implement an {{TS-lang|accept}} method accepting an object implementing the interface {{TS-lang|AnimalVisitor}} (adding non-local [[Boilerplate code|boilerplate code]]).
The function {{TS-lang|animalToFood}} would be realized as the {{TS-lang|visit}} method of an implementation of {{TS-lang|AnimalVisitor}}.
Unfortunately, the connection between the input type ({{TS-lang|Chicken}} or {{TS-lang|Cow}}) and the result type ({{TS-lang|Egg}} or {{TS-lang|Milk}}) 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|parametric polymorphism]], or [[Duck typing|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>(x : \sigma) \cap \tau</math>, is a [[Dependent type|dependent type]] in which the type <math>\tau</math> may depend on the term variable <math>x</math>.<ref name=K03>{{cite conference |title=Dependent intersection: A new way of defining records in type theory |last1=Kopylov |first1=Alexei |year=2003 |publisher=IEEE Computer Society |book-title=18th IEEE Symposium on Logic in Computer Science |pages=86–95 |conference=LICS 2003 |doi=10.1109/LICS.2003.1210048 |citeseerx=10.1.1.89.4223 }}</ref>
In particular, if a term <math>M</math> has the dependent intersection type <math>(x : \sigma) \cap \tau</math>, then the term <math>M</math> has ''both'' the type <math>\sigma</math> and the type <math>\tau[x := M]</math>, where <math>\tau[x := M]</math> is the type which results from replacing all occurrences of the term variable <math>x</math> in <math>\tau</math> by the term <math>M</math>.

=== Scala example ===
[[Scala (programming language)|Scala]] supports type declarations <ref>{{cite web |url=https://www.scala-lang.org/files/archive/spec/2.12/04-basic-declarations-and-definitions.html#type-declarations-and-type-aliases |title=Type declarations in Scala |access-date=2019-08-15}}</ref> as object members. This allows a type of an object member to depend on the value of another member, which is called a ''path-dependent type''.<ref>
{{cite book |last1=Amin |first1=Nada |last2=Grütter |first2=Samuel |last3=Odersky |first3=Martin |last4=Rompf |first4=Tiark |last5=Stucki |first5=Sandro  |title=A List of Successes That Can Change the World |chapter=The Essence of Dependent Object Types |series=Lecture Notes in Computer Science |volume=9600 |pages=249–272 |year=2016 |publisher=Springer |doi=10.1007/978-3-319-30936-1_14 |isbn=978-3-319-30935-4 |url=https://infoscience.epfl.ch/record/215280/files/paper_1.pdf }}</ref>
For example, the following program text defines a Scala trait <source lang="Scala" inline>Witness</source>, which can be used to implement the [[Singleton pattern|singleton pattern]].<ref>{{cite web |url=https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/singletons.scala |title=Singletons in the Scala shapeless library |website=[[GitHub]] |access-date=2019-08-15}}</ref>
<source lang="Scala">
trait Witness {
  type T
  val value: T {}
}
</source>
The above trait <source lang="Scala" inline>Witness</source> declares the member <source lang="Scala" inline>T</source>, which can be assigned a ''type'' as its value, and the member <source lang="Scala" inline>value</source>, which can be assigned a value of type <source lang="Scala" inline>T</source>.
The following program text defines an object <source lang="Scala" inline>booleanWitness</source> as instance of the above trait <source lang="Scala" inline>Witness </source>.
The object <source lang="Scala" inline>booleanWitness</source> defines the type <source lang="Scala" inline>T</source> as <source lang="Scala" inline>Boolean</source> and the value <source lang="Scala" inline>value</source> as <source lang="Scala" inline>true</source>.
For example, executing <source lang="Scala" inline>System.out.println(booleanWitness.value)</source> prints <source lang="Scala" inline>true</source> on the console.
<source lang="Scala">
object booleanWitness extends Witness {
  type T = Boolean
  val value = true
}
</source>

Let <math>\langle \textsf{x} : \sigma \rangle</math> be the type (specifically, a [[Record (computer science)|record type]]) of objects having the member <math>\textsf{x}</math> of type <math>\sigma</math>.
In the above example, the object <source lang="Scala" inline>booleanWitness</source> can be assigned the dependent intersection type <math>(x : \langle \textsf{T} : \text{Type} \rangle) \cap \langle \textsf{value} : x.\textsf{T} \rangle</math>.
The reasoning is as follows. The object <source lang="Scala" inline>booleanWitness</source> has the member <source lang="Scala" inline>T</source> that is assigned the type <source lang="Scala" inline>Boolean</source> as its value.
Since <source lang="Scala" inline>Boolean</source> is a type, the object <source lang="Scala" inline>booleanWitness</source> has the type <math>\langle \textsf{T} : \text{Type} \rangle</math>.
Additionally, the object <source lang="Scala" inline>booleanWitness</source> has the member <source lang="Scala" inline>value</source> that is assigned the value <source lang="Scala" inline>true</source> of type <source lang="Scala" inline>Boolean</source>.
Since the value of <source lang="Scala" inline>booleanWitness.T</source> is <source lang="Scala" inline>Boolean</source>, the object <source lang="Scala" inline>booleanWitness</source> has the type <math>\langle \textsf{value} : \textsf{booleanWitness.T} \rangle</math>.
Overall, the object <source lang="Scala" inline>booleanWitness</source> has the intersection type <math>\langle \textsf{T} : \text{Type} \rangle \cap \langle \textsf{value} : \textsf{booleanWitness.T} \rangle</math>.
Therefore, presenting self-reference as dependency, the object <source lang="Scala" inline>booleanWitness</source> has the dependent intersection type <math>(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''.<ref>{{cite conference |title=Dependently typed records for representing mathematical structure |last1=Pollack |first1=Robert |publisher=Springer |book-title=Theorem Proving in Higher Order Logics, 13th International Conference |pages=462–479 |conference=TPHOLs 2000 |year=2000 |doi=10.1007/3-540-44659-1_29 }}</ref>
In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept.<ref name=K03/>

== Intersection of a type family ==
An '''intersection of a type family''', denoted <math display="inline">\bigcap_{x : \sigma} \tau</math>, is a [[Dependent type|dependent type]] in which the type <math>\tau</math> may depend on the term variable <math>x</math>. In particular, if a term <math>M</math> has the type <math display="inline">\bigcap_{x : \sigma} \tau</math>, then for ''each'' term <math>N</math> of type <math>\sigma</math>, the term <math>M</math> has the type <math>\tau[x := N]</math>. This notion is also called ''implicit [[Dependent type#Pi type|Pi type]]'',<ref>{{cite journal |last1=Stump |first1=Aaron |year=2018 |title=From realizability to induction via dependent intersection |journal=Annals of Pure and Applied Logic |volume=169 |issue=7 |pages=637–655 |doi=10.1016/j.apal.2018.03.002 |doi-access=free }}</ref> observing that the argument <math>N</math> is not kept at term level.

== Comparison of languages with intersection types ==
{| class="wikitable sortable"
|-
! Language !! Actively developed !! Paradigm(s) !! Status !! Features 
|-
| [[C Sharp (programming language)|C#]] || {{yes}}<ref>{{cite web |url=http://csharp.net/ |title=C# Guide |access-date=2019-08-08}}</ref> ||
* [[Functional programming|Functional]]
* [[Imperative programming|Imperative]]
* [[Object-oriented programming|Object-oriented]]
| {{maybe|Under discussion}}<ref>{{cite web |url=https://github.com/dotnet/csharplang/issues/399 |title=Discussion: Union and Intersection types in C Sharp |website=[[GitHub]] |access-date=2019-08-08}}</ref> || Additionally, generic type parameters can have constraints that require their (monomorphized) type-arguments to implement multiple interfaces, whereupon the runtime type represented by the generic type parameter becomes an intersection-type of all listed interfaces.
|-
| [[Ceylon (programming language)|Ceylon]] || {{No}}<ref>{{cite web|url=https://projects.eclipse.org/projects/technology.ceylon/|title=Eclipse Ceylon™|date=19 July 2017 |access-date=2023-08-16}}</ref> || 
* [[Object-oriented programming|Object-oriented]] 
| {{yes|Supported}}<ref name=Cey>{{cite web |url=https://ceylon-lang.org/documentation/tour/types/#intersection_types |title=Intersection Types in Ceylon |date=19 July 2017 |access-date=2019-08-08}}</ref> ||
* Type refinement
* Interface composition
* Subtyping in width
|-
| [[F Sharp (programming language)|F#]] || {{yes}}<ref>{{cite web |url=http://fsharp.org/ |title=F# Software Foundation |access-date=2019-08-08}}</ref> ||
* [[Functional programming|Functional]]
* [[Imperative programming|Imperative]]
* [[Object-oriented programming|Object-oriented]]
| {{maybe|Under discussion}}<ref>{{cite web |url=https://github.com/fsharp/fslang-suggestions/issues/600 |title=Add Intersection Types to F Sharp |website=[[GitHub]] |access-date=2019-08-08}}</ref> || {{dunno}}
|-
| Flow || {{yes}}<ref>{{cite web|url=https://flow.org/en/|title=Flow: A Static Type Checker for JavaScript|access-date=2019-08-08}}</ref> || 
* [[Functional programming|Functional]]
* [[Imperative programming|Imperative]]
* [[Object-oriented programming|Object-oriented]]
* [[Scripting language|Scripting]]
| {{yes|Supported}}<ref>{{cite web |url=https://flow.org/en/docs/types/intersections/#intersection-type-syntax |title=Intersection Type Syntax in Flow |access-date=2019-08-08}}</ref> ||
* Type refinement
* Interface composition
|-
| [[Forsythe (programming language)|Forsythe]] || {{no}} || 
* [[Imperative programming|Imperative]] 
| {{yes|Supported}}<ref>Reynolds, J. C. (1988). Preliminary design of the programming language Forsythe.</ref>
|
* Function type intersection
* Distributive, co- and contravariant function type subtyping
|-
| [[Java (programming language)|Java]] || {{yes}}<ref>{{cite web|url=https://www.oracle.com/java/|title=Java Software |access-date=2019-08-08}}</ref> 
| 
* [[Imperative programming|Imperative]]  
* [[Object-oriented programming|Object-oriented]] 
| {{yes|Supported}}<ref>{{cite web |url=https://docs.oracle.com/en/java/javase/12/docs/api/java.compiler/javax/lang/model/type/IntersectionType.html |title=IntersectionType (Java SE 12 & JDK 12) |access-date=2019-08-01}}</ref> 
| 
* Type refinement
* Interface composition
* Subtyping in width
|-
|-
| [[Organization:PHP|PHP]] || {{yes}}<ref>{{cite web|url=https://php.net|title=php.net}}</ref> 
| 
* [[Functional programming|Functional]] 
* [[Imperative programming|Imperative]] 
* [[Object-oriented programming|Object-oriented]]
* [[Scripting language|Scripting]]
| {{yes|Supported}}<ref>{{cite web |url=https://php.watch/versions/8.1/intersection-types |title=PHP.Watch - PHP 8.1: Intersection Types}}</ref>
| 
* Type refinement
* Interface composition
|-
| [[Scala (programming language)|Scala]] || {{yes}}<ref>{{cite web|url=https://scala-lang.org/|title=The Scala Programming Language|access-date=2019-08-08}}</ref> 
| 
* [[Functional programming|Functional]]  
* [[Imperative programming|Imperative]]  
* [[Object-oriented programming|Object-oriented]] 
| {{yes|Supported}}<ref>{{cite web |url=https://www.scala-lang.org/files/archive/spec/2.12/03-types.html#compound-types |title=Compound Types in Scala |access-date=2019-08-01}}</ref><ref>{{cite web |url=http://dotty.epfl.ch/docs/reference/new-types/intersection-types.html |title=Intersection Types in Dotty |access-date=2019-08-01}}</ref> 
| 
* Type refinement
* Trait composition
* Subtyping in width
|-
| TypeScript || {{yes}}<ref>{{cite web |url=https://www.typescriptlang.org/ |title=TypeScript - JavaScript that scales. |access-date=2019-08-01}}</ref> ||
* [[Functional programming|Functional]]
* [[Imperative programming|Imperative]]
* [[Object-oriented programming|Object-oriented]]
* [[Scripting language|Scripting]]
| {{yes|Supported}}<ref name=TS>{{cite web |url=https://www.typescriptlang.org/docs/handbook/advanced-types.html#intersection-types |title=Intersection Types in TypeScript |access-date=2019-08-01}}</ref> ||
* Arbitrary type intersection
* Interface composition
* Subtyping in width and depth
|-
| [[Whiley (programming language)|Whiley]] || {{yes}}<ref>{{cite web |url=http://whiley.org/ |title=Whiley: an Open Source Programming Language with Extended Static Checking |access-date=2019-08-01}}</ref> ||
* [[Functional programming|Functional]]
* [[Imperative programming|Imperative]]
| {{yes|Supported}}<ref>{{cite web |url=http://whiley.org/download/WhileyLanguageSpec.pdf |title=Whiley language specification |access-date=2019-08-01}}</ref> || {{dunno}}
|}

==References==
{{RefList}}

{{Data types}}

<!--- Categories --->
[[Category:Type theory]]
[[Category:Type systems]]
[[Category:Data types]]
[[Category:Composite data types]]
[[Category:Polymorphism (computer science)]]

{{Sourceattribution|Intersection type}}