Intersection type

<h2 id="typescript-example">TypeScript example</h2>
<a href="/facts/TypeScript/W9J27V1N">TypeScript</a> supports intersection types,<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a> improving expressiveness of the type system and reducing potential class hierarchy size, demonstrated as follows.
The following program code defines the classes Chicken, Cow, and RandomNumberGenerator that each have a method produce returning an object of either type Egg, Milk, or number.
Additionally, the functions eatEgg and drinkMilk require arguments of type Egg and Milk, 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 <a href="/facts/Ad_hoc_polymorphism/C15g3Bvz">ad hoc polymorphic</a> function animalToFood that invokes the member function produce of the given object animal.
The function animalToFood has two type annotations, namely ((_: Chicken) => Egg) and ((_: Cow) => Milk), connected via the intersection type constructor &.
Specifically, animalToFood when applied to an argument of type Chicken returns an object of type Egg, and when applied to an argument of type Cow returns an object of type Milk.
Ideally, animalToFood should not be applicable to any object having (possibly by chance) a produce 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 <a href="/facts/Type_safety/WxmEKq8R">type safe</a> 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:

<ul><li>Lines 1–3 create objects chicken, cow, and randomNumberGenerator of their respective type.</li>
<li>Lines 5–7 print for the previously created objects the respective results (provided as comments) when invoking produce.</li>
<li>Line 9 (resp. 10) demonstrates type safe use of the method animalToFood applied to chicken (resp. cow).</li>
<li>Line 11, if uncommented, would result in a type error at compile time. Although the implementation of animalToFood could invoke the produce method of randomNumberGenerator, the type annotation of animalToFood disallows it. This is in accordance with the intended meaning of animalToFood.</li>
<li>Line 13 (resp. 15) demonstrates that applying animalToFood to chicken (resp. cow) results in an object of type Egg (resp. Milk).</li>
<li>Line 14 (resp. 16) demonstrates that applying animalToFood to cow (resp. chicken) does not result in an object of type Egg (resp. Milk). Therefore, if uncommented, line 14 (resp. 16) would result in a type error at compile time.</li></ul>
<h3>Comparison to inheritance</h3>
The above minimalist example can be realized using <a href="/facts/Inheritance_(object-oriented_programming)/a7R1xv8n">inheritance</a>, for instance by deriving the classes Chicken and Cow from a base class Animal.
However, in a larger setting, this could be disadvantageous.
Introducing new classes into a class hierarchy is not necessarily justified for <a href="/facts/Cross-cutting_concern/zUWmQsQm">cross-cutting concerns</a>, or maybe outright impossible, for example when using an external library. 
Imaginably, the above example could be extended with the following classes:

<ul><li>a class Horse that does not have a produce method;</li>
<li>a class Sheep that has a produce method returning Wool;</li>
<li>a class Pig that has a produce method, which can be used only once, returning Meat.</li></ul>
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.

<h3>Comparison to duck typing</h3>
The above minimalist example already shows that <a href="/facts/Duck_typing/tcuo8Ywq">duck typing</a> is less suited to realize the given scenario.
While the class RandomNumberGenerator contains a produce method, the object randomNumberGenerator should not be a valid argument for animalToFood.
The above example can be realized using duck typing, for instance by introducing a new field argumentForAnimalToFood to the classes Chicken and Cow signifying that objects of corresponding type are valid arguments for animalToFood.
However, this would not only increase the size of the respective classes (especially with the introduction of more methods similar to animalToFood), but is also a non-local approach with respect to animalToFood.

<h3>Comparison to function overloading</h3>
The above example can be realized using <a href="/facts/Function_overloading/wL27p4rD">function overloading</a>, for instance by implementing two methods animalToFood(animal: Chicken): Egg and animalToFood(animal: Cow): Milk.
In TypeScript, such a solution is almost identical to the provided example. 
Other programming languages, such as <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a>, require distinct implementations of the overloaded method.
This may lead to either <a href="/facts/Code_duplication/adzaD7R2">code duplication</a> or <a href="/facts/Boilerplate_code/xbYAfVbW">boilerplate code</a>.

<h3>Comparison to the visitor pattern</h3>
The above example can be realized using the <a href="/facts/Visitor_pattern/GsrVLERl">visitor pattern</a>.
It would require each animal class to implement an accept method accepting an object implementing the interface AnimalVisitor (adding non-local <a href="/facts/Boilerplate_code/xbYAfVbW">boilerplate code</a>).
The function animalToFood would be realized as the visit method of an implementation of AnimalVisitor.
Unfortunately, the connection between the input type (Chicken or Cow) and the result type (Egg or Milk) would be difficult to represent.

<h3>Limitations</h3>
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, <a href="/facts/Parametric_polymorphism/ETb0G1zd">parametric polymorphism</a>, or <a href="/facts/Duck_typing/tcuo8Ywq">duck typing</a>, then the verbose nature of intersection types is unfavorable.
Therefore, intersection types should be considered complementary to existing specification methods.

<h2 id="dependent-intersection-type">Dependent intersection type</h2>
A dependent intersection type, denoted 
 
 
 
 (
 x
 :
 σ
 )
 ∩
 τ
 
 
 {\displaystyle (x:\sigma )\cap \tau }
 
, is a <a href="/facts/Dependent_type/wCeQI7ds">dependent type</a> in which the type 
 
 
 
 τ
 
 
 {\displaystyle \tau }
 
 may depend on the term variable 
 
 
 
 x
 
 
 {\displaystyle x}
 
.<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a>
In particular, if a term 
 
 
 
 M
 
 
 {\displaystyle M}
 
 has the dependent intersection type 
 
 
 
 (
 x
 :
 σ
 )
 ∩
 τ
 
 
 {\displaystyle (x:\sigma )\cap \tau }
 
, then the term 
 
 
 
 M
 
 
 {\displaystyle M}
 
 has both the type 
 
 
 
 σ
 
 
 {\displaystyle \sigma }
 
 and the type 
 
 
 
 τ
 [
 x
 :=
 M
 ]
 
 
 {\displaystyle \tau [x:=M]}
 
, where 
 
 
 
 τ
 [
 x
 :=
 M
 ]
 
 
 {\displaystyle \tau [x:=M]}
 
 is the type which results from replacing all occurrences of the term variable 
 
 
 
 x
 
 
 {\displaystyle x}
 
 in 
 
 
 
 τ
 
 
 {\displaystyle \tau }
 
 by the term 
 
 
 
 M
 
 
 {\displaystyle M}
 
.

<h3>Scala example</h3>
<a href="/facts/Scala_(programming_language)/ebL8o6AK">Scala</a> supports type declarations <a class="footnote-ref" id="fnref:7" href="#fn:7">7</a> 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.<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a>
For example, the following program text defines a Scala trait Witness, which can be used to implement the <a href="/facts/Singleton_pattern/dl70cvTu">singleton pattern</a>.<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a>

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 
 
 
 
 ⟨
 
 
 x
 
 
 :
 σ
 ⟩
 
 
 {\displaystyle \langle {\textsf {x}}:\sigma \rangle }
 
 be the type (specifically, a <a href="/facts/Record_(computer_science)/1fvSgenB">record type</a>) of objects having the member 
 
 
 
 
 
 x
 
 
 
 
 {\displaystyle {\textsf {x}}}
 
 of type 
 
 
 
 σ
 
 
 {\displaystyle \sigma }
 
.
In the above example, the object booleanWitness can be assigned the dependent intersection type 
 
 
 
 (
 x
 :
 ⟨
 
 
 T
 
 
 :
 
 Type
 
 ⟩
 )
 ∩
 ⟨
 
 
 value
 
 
 :
 x
 .
 
 
 T
 
 
 ⟩
 
 
 {\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle }
 
.
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 
 
 
 
 ⟨
 
 
 T
 
 
 :
 
 Type
 
 ⟩
 
 
 {\displaystyle \langle {\textsf {T}}:{\text{Type}}\rangle }
 
.
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 
 
 
 
 ⟨
 
 
 value
 
 
 :
 
 
 booleanWitness.T
 
 
 ⟩
 
 
 {\displaystyle \langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle }
 
.
Overall, the object booleanWitness has the intersection type 
 
 
 
 ⟨
 
 
 T
 
 
 :
 
 Type
 
 ⟩
 ∩
 ⟨
 
 
 value
 
 
 :
 
 
 booleanWitness.T
 
 
 ⟩
 
 
 {\displaystyle \langle {\textsf {T}}:{\text{Type}}\rangle \cap \langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle }
 
.
Therefore, presenting self-reference as dependency, the object booleanWitness has the dependent intersection type 
 
 
 
 (
 x
 :
 ⟨
 
 
 T
 
 
 :
 
 Type
 
 ⟩
 )
 ∩
 ⟨
 
 
 value
 
 
 :
 x
 .
 
 
 T
 
 
 ⟩
 
 
 {\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle }
 
.
Alternatively, the above minimalistic example can be described using dependent record types.<a class="footnote-ref" id="fnref:10" href="#fn:10">10</a>
In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept.<a class="footnote-ref" id="fnref:11" href="#fn:11">11</a>

<h2 id="intersection-of-a-type-family">Intersection of a type family</h2>
An intersection of a type family, denoted 
 
 
 
 
 ⋂
 
 x
 :
 σ
 
 
 τ
 
 
 {\textstyle \bigcap _{x:\sigma }\tau }
 
, is a <a href="/facts/Dependent_type/wCeQI7ds">dependent type</a> in which the type 
 
 
 
 τ
 
 
 {\displaystyle \tau }
 
 may depend on the term variable 
 
 
 
 x
 
 
 {\displaystyle x}
 
. In particular, if a term 
 
 
 
 M
 
 
 {\displaystyle M}
 
 has the type 
 
 
 
 
 ⋂
 
 x
 :
 σ
 
 
 τ
 
 
 {\textstyle \bigcap _{x:\sigma }\tau }
 
, then for each term 
 
 
 
 N
 
 
 {\displaystyle N}
 
 of type 
 
 
 
 σ
 
 
 {\displaystyle \sigma }
 
, the term 
 
 
 
 M
 
 
 {\displaystyle M}
 
 has the type 
 
 
 
 τ
 [
 x
 :=
 N
 ]
 
 
 {\displaystyle \tau [x:=N]}
 
. This notion is also called implicit <a href="/facts/Dependent_type/wCeQI7ds">Pi type</a>,<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a> observing that the argument 
 
 
 
 N
 
 
 {\displaystyle N}
 
 is not kept at term level.

<h2 id="comparison-of-languages-with-intersection-types">Comparison of languages with intersection types</h2>
<table><tbody><tr><th>Language</th><th>Actively developed</th><th>Paradigm(s)</th><th>Status</th><th>Features</th></tr><tr><td><a href="/facts/C_Sharp_(programming_language)/UC2gxeyb">C#</a></td><td>Yes<a class="footnote-ref" id="fnref:13" href="#fn:13">13</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li></ul></td><td>Under discussion<a class="footnote-ref" id="fnref:14" href="#fn:14">14</a></td><td>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.</td></tr><tr><td><a href="/facts/Ceylon_(programming_language)/cygDphIa">Ceylon</a></td><td>No<a class="footnote-ref" id="fnref:15" href="#fn:15">15</a></td><td><ul><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:16" href="#fn:16">16</a></td><td><ul><li>Type refinement</li><li>Interface composition</li><li>Subtyping in width</li></ul></td></tr><tr><td><a href="/facts/F_Sharp_(programming_language)/jdXHnYz5">F#</a></td><td>Yes<a class="footnote-ref" id="fnref:17" href="#fn:17">17</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li></ul></td><td>Under discussion<a class="footnote-ref" id="fnref:18" href="#fn:18">18</a></td><td>?</td></tr><tr><td>Flow</td><td>Yes<a class="footnote-ref" id="fnref:19" href="#fn:19">19</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li><li><a href="/facts/Scripting_language/8pF4ajBL">Scripting</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:20" href="#fn:20">20</a></td><td><ul><li>Type refinement</li><li>Interface composition</li></ul></td></tr><tr><td><a href="/facts/Forsythe_(programming_language)/6cdgIrBx">Forsythe</a></td><td>No</td><td><ul><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:21" href="#fn:21">21</a></td><td><ul><li>Function type intersection</li><li>Distributive, co- and contravariant function type subtyping</li></ul></td></tr><tr><td><a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a></td><td>Yes<a class="footnote-ref" id="fnref:22" href="#fn:22">22</a></td><td><ul><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:23" href="#fn:23">23</a></td><td><ul><li>Type refinement</li><li>Interface composition</li><li>Subtyping in width</li></ul></td></tr><tr><td><a href="/facts/PHP/vU6YRJX0">PHP</a></td><td>Yes<a class="footnote-ref" id="fnref:24" href="#fn:24">24</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li><li><a href="/facts/Scripting_language/8pF4ajBL">Scripting</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:25" href="#fn:25">25</a></td><td><ul><li>Type refinement</li><li>Interface composition</li></ul></td></tr><tr><td><a href="/facts/Scala_(programming_language)/ebL8o6AK">Scala</a></td><td>Yes<a class="footnote-ref" id="fnref:26" href="#fn:26">26</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:27" href="#fn:27">27</a><a class="footnote-ref" id="fnref:28" href="#fn:28">28</a></td><td><ul><li>Type refinement</li><li>Trait composition</li><li>Subtyping in width</li></ul></td></tr><tr><td><a href="/facts/Microsoft_TypeScript/W9J27V1N">TypeScript</a></td><td>Yes<a class="footnote-ref" id="fnref:29" href="#fn:29">29</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li><li><a href="/facts/Object-oriented_programming/TxNMEcao">Object-oriented</a></li><li><a href="/facts/Scripting_language/8pF4ajBL">Scripting</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:30" href="#fn:30">30</a></td><td><ul><li>Arbitrary type intersection</li><li>Interface composition</li><li>Subtyping in width and depth</li></ul></td></tr><tr><td><a href="/facts/Whiley_(programming_language)/qzFD6d6t">Whiley</a></td><td>Yes<a class="footnote-ref" id="fnref:31" href="#fn:31">31</a></td><td><ul><li><a href="/facts/Functional_programming/cdxqPEIM">Functional</a></li><li><a href="/facts/Imperative_programming/6b5dUnE1">Imperative</a></li></ul></td><td>Supported<a class="footnote-ref" id="fnref:32" href="#fn:32">32</a></td><td>?</td></tr></tbody></table>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Barendregt, Henk; Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1983). "A filter lambda model and the completeness of type assignment". Journal of Symbolic Logic. 48 (4): 931–940. doi:10.2307/2273659. JSTOR 2273659. S2CID 45660117. <a href="/wiki/Mariangiola_Dezani-Ciancaglini" target="_blank">/wiki/Mariangiola_Dezani-Ciancaglini</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Palsberg, Jens (2012). "Overloading is NP-Complete". Logic and Program Semantics. Lecture Notes in Computer Science. Vol. 7230. pp. 204–218. doi:10.1007/978-3-642-29485-3_13. ISBN 978-3-642-29484-6. <a href="978-3-642-29484-6" target="_blank">978-3-642-29484-6</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013). Lambda Calculus with Types. Cambridge University Press. pp. 1–. ISBN 978-0-521-76614-2. <a href="978-0-521-76614-2" target="_blank">978-0-521-76614-2</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">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. <a href="https://doi.org/10.1305%2Fndjfl%2F1040067315" target="_blank">https://doi.org/10.1305%2Fndjfl%2F1040067315</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">"Intersection Types in TypeScript". Retrieved 2019-08-01. <a href="https://www.typescriptlang.org/docs/handbook/advanced-types.html#intersection-types" target="_blank">https://www.typescriptlang.org/docs/handbook/advanced-types.html#intersection-types</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". 18th IEEE Symposium on Logic in Computer Science. LICS 2003. IEEE Computer Society. pp. 86–95. CiteSeerX 10.1.1.89.4223. doi:10.1109/LICS.2003.1210048. <a href="/wiki/CiteSeerX_(identifier)" target="_blank">/wiki/CiteSeerX_(identifier)</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">"Type declarations in Scala". Retrieved 2019-08-15. <a href="https://www.scala-lang.org/files/archive/spec/2.12/04-basic-declarations-and-definitions.html#type-declarations-and-type-aliases" target="_blank">https://www.scala-lang.org/files/archive/spec/2.12/04-basic-declarations-and-definitions.html#type-declarations-and-type-aliases</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Amin, Nada; Grütter, Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro (2016). "The Essence of Dependent Object Types". A List of Successes That Can Change the World (PDF). Lecture Notes in Computer Science. Vol. 9600. Springer. pp. 249–272. doi:10.1007/978-3-319-30936-1_14. ISBN 978-3-319-30935-4. <a href="978-3-319-30935-4" target="_blank">978-3-319-30935-4</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">"Singletons in the Scala shapeless library". GitHub. Retrieved 2019-08-15. <a href="https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/singletons.scala" target="_blank">https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/singletons.scala</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Pollack, Robert (2000). "Dependently typed records for representing mathematical structure". Theorem Proving in Higher Order Logics, 13th International Conference. TPHOLs 2000. Springer. pp. 462–479. doi:10.1007/3-540-44659-1_29. <a href="/wiki/Doi_(identifier)" target="_blank">/wiki/Doi_(identifier)</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". 18th IEEE Symposium on Logic in Computer Science. LICS 2003. IEEE Computer Society. pp. 86–95. CiteSeerX 10.1.1.89.4223. doi:10.1109/LICS.2003.1210048. <a href="/wiki/CiteSeerX_(identifier)" target="_blank">/wiki/CiteSeerX_(identifier)</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">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. <a href="https://doi.org/10.1016%2Fj.apal.2018.03.002" target="_blank">https://doi.org/10.1016%2Fj.apal.2018.03.002</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
<li id="fn:13">"C# Guide". Retrieved 2019-08-08. <a href="http://csharp.net/" target="_blank">http://csharp.net/</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></li>
<li id="fn:14">"Discussion: Union and Intersection types in C Sharp". GitHub. Retrieved 2019-08-08. <a href="https://github.com/dotnet/csharplang/issues/399" target="_blank">https://github.com/dotnet/csharplang/issues/399</a> <a href="#fnref:14" class="footnote-back-ref">↩</a></li>
<li id="fn:15">"Eclipse Ceylon™". 19 July 2017. Retrieved 2023-08-16. <a href="https://projects.eclipse.org/projects/technology.ceylon/" target="_blank">https://projects.eclipse.org/projects/technology.ceylon/</a> <a href="#fnref:15" class="footnote-back-ref">↩</a></li>
<li id="fn:16">"Intersection Types in Ceylon". 19 July 2017. Retrieved 2019-08-08. <a href="https://ceylon-lang.org/documentation/tour/types/#intersection_types" target="_blank">https://ceylon-lang.org/documentation/tour/types/#intersection_types</a> <a href="#fnref:16" class="footnote-back-ref">↩</a></li>
<li id="fn:17">"F# Software Foundation". Retrieved 2019-08-08. <a href="http://fsharp.org/" target="_blank">http://fsharp.org/</a> <a href="#fnref:17" class="footnote-back-ref">↩</a></li>
<li id="fn:18">"Add Intersection Types to F Sharp". GitHub. Retrieved 2019-08-08. <a href="https://github.com/fsharp/fslang-suggestions/issues/600" target="_blank">https://github.com/fsharp/fslang-suggestions/issues/600</a> <a href="#fnref:18" class="footnote-back-ref">↩</a></li>
<li id="fn:19">"Flow: A Static Type Checker for JavaScript". Archived from the original on 2022-04-08. Retrieved 2019-08-08. <a href="https://web.archive.org/web/20220408204727/https://flow.org/en/" target="_blank">https://web.archive.org/web/20220408204727/https://flow.org/en/</a> <a href="#fnref:19" class="footnote-back-ref">↩</a></li>
<li id="fn:20">"Intersection Type Syntax in Flow". Retrieved 2019-08-08. <a href="https://flow.org/en/docs/types/intersections/#intersection-type-syntax" target="_blank">https://flow.org/en/docs/types/intersections/#intersection-type-syntax</a> <a href="#fnref:20" class="footnote-back-ref">↩</a></li>
<li id="fn:21">Reynolds, J. C. (1988). Preliminary design of the programming language Forsythe. <a href="#fnref:21" class="footnote-back-ref">↩</a></li>
<li id="fn:22">"Java Software". Retrieved 2019-08-08. <a href="https://www.oracle.com/java/" target="_blank">https://www.oracle.com/java/</a> <a href="#fnref:22" class="footnote-back-ref">↩</a></li>
<li id="fn:23">"IntersectionType (Java SE 12 & JDK 12)". Retrieved 2019-08-01. <a href="https://docs.oracle.com/en/java/javase/12/docs/api/java.compiler/javax/lang/model/type/IntersectionType.html" target="_blank">https://docs.oracle.com/en/java/javase/12/docs/api/java.compiler/javax/lang/model/type/IntersectionType.html</a> <a href="#fnref:23" class="footnote-back-ref">↩</a></li>
<li id="fn:24">"php.net". <a href="https://php.net" target="_blank">https://php.net</a> <a href="#fnref:24" class="footnote-back-ref">↩</a></li>
<li id="fn:25">"PHP.Watch - PHP 8.1: Intersection Types". <a href="https://php.watch/versions/8.1/intersection-types" target="_blank">https://php.watch/versions/8.1/intersection-types</a> <a href="#fnref:25" class="footnote-back-ref">↩</a></li>
<li id="fn:26">"The Scala Programming Language". Retrieved 2019-08-08. <a href="https://scala-lang.org/" target="_blank">https://scala-lang.org/</a> <a href="#fnref:26" class="footnote-back-ref">↩</a></li>
<li id="fn:27">"Compound Types in Scala". Retrieved 2019-08-01. <a href="https://www.scala-lang.org/files/archive/spec/2.12/03-types.html#compound-types" target="_blank">https://www.scala-lang.org/files/archive/spec/2.12/03-types.html#compound-types</a> <a href="#fnref:27" class="footnote-back-ref">↩</a></li>
<li id="fn:28">"Intersection Types in Dotty". Retrieved 2019-08-01. <a href="http://dotty.epfl.ch/docs/reference/new-types/intersection-types.html" target="_blank">http://dotty.epfl.ch/docs/reference/new-types/intersection-types.html</a> <a href="#fnref:28" class="footnote-back-ref">↩</a></li>
<li id="fn:29">"TypeScript - JavaScript that scales". Retrieved 2019-08-01. <a href="https://www.typescriptlang.org/" target="_blank">https://www.typescriptlang.org/</a> <a href="#fnref:29" class="footnote-back-ref">↩</a></li>
<li id="fn:30">"Intersection Types in TypeScript". Retrieved 2019-08-01. <a href="https://www.typescriptlang.org/docs/handbook/advanced-types.html#intersection-types" target="_blank">https://www.typescriptlang.org/docs/handbook/advanced-types.html#intersection-types</a> <a href="#fnref:30" class="footnote-back-ref">↩</a></li>
<li id="fn:31">"Whiley: an Open Source Programming Language with Extended Static Checking". Retrieved 2019-08-01. <a href="http://whiley.org/" target="_blank">http://whiley.org/</a> <a href="#fnref:31" class="footnote-back-ref">↩</a></li>
<li id="fn:32">"Whiley language specification" (PDF). Retrieved 2019-08-01. <a href="http://whiley.org/download/WhileyLanguageSpec.pdf" target="_blank">http://whiley.org/download/WhileyLanguageSpec.pdf</a> <a href="#fnref:32" class="footnote-back-ref">↩</a></li>
</ol>

Intersection type open-in-new

Intersection type