Intype theory, anintersection type can be allocated to values that can be assigned both the type${\displaystyle \sigma }$ and the type${\displaystyle \tau }$. This value can be given the intersection type${\displaystyle \sigma \cap \tau }$ in anintersection type system.^[1]Generally, if the ranges of values of two types overlap, then a value belonging to theintersection of the two ranges can be assigned theintersection type of these two types. Such a value can be safely passed as argument to functions expectingeither of the two types.For example, inJava the classBoolean implements both theSerializable and theComparable interfaces. Therefore, an object of typeBoolean can be safely passed to functions expecting an argument of typeSerializable and to functions expecting an argument of typeComparable.

Intersection types arecomposite data types. Similar toproduct types, they are used to assign several types to an object.However, product types are assigned totuples, 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 arerefinement types.

Intersection types are useful for describingoverloaded functions.^[2] For example, ifnumber=>number is the type of function taking a number as an argument and returning a number, andstring=>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, includingCeylon, Flow,Java,Scala,TypeScript, andWhiley (seecomparison of languages with intersection types), use intersection types to combine interface specifications and to expressad hoc polymorphism.Complementingparametric polymorphism, intersection types may be used to avoid class hierarchy pollution fromcross-cutting concerns and reduceboilerplate code, as shown in theTypeScript example below.

Thetype theoretic study of intersection types is referred to as theintersection type discipline.^[3]Remarkably, program termination can be precisely characterized using intersection types.^[4] Consequently,type inference for infinite-intersection types isundecidable, but it is decidable for all finite rank intersection types.^[5]

TypeScript supports intersection types,^[6] improving expressiveness of the type system and reducing potential class hierarchy size, demonstrated as follows.

The following program code defines the classesChicken,Cow, andRandomNumberGenerator that each have a methodproduce returning an object of either typeEgg,Milk, ornumber.Additionally, the functionseatEgg anddrinkMilk require arguments of typeEgg andMilk, respectively.

classEgg{privatekind:"Egg"}classMilk{privatekind:"Milk"}// produces eggsclassChicken{produce(){returnnewEgg();}}// produces milkclassCow{produce(){returnnewMilk();}}// produces a random numberclassRandomNumberGenerator{produce(){returnMath.random();}}// requires an eggfunctioneatEgg(egg:Egg){return"I ate an egg.";}// requires milkfunctiondrinkMilk(milk:Milk){return"I drank some milk.";}

The following program code defines thead hoc polymorphic functionanimalToFood that invokes the member functionproduce of the given objectanimal.The functionanimalToFood hastwo type annotations, namely((_:Chicken)=>Egg) and((_:Cow)=>Milk), connected via the intersection type constructor&.Specifically,animalToFood when applied to an argument of typeChicken returns an object of typeEgg, and when applied to an argument of typeCow returns an object of typeMilk.Ideally,animalToFood should not be applicable to any object having (possibly by chance) aproduce method.

// given a chicken, produces an egg; given a cow, produces milkletanimalToFood:((_:Chicken)=>Egg)&((_:Cow)=>Milk)=function(animal:any){returnanimal.produce();};

Finally, the following program code demonstratestype safe use of the above definitions.

varchicken=newChicken();varcow=newCow();varrandomNumberGenerator=newRandomNumberGenerator();console.log(chicken.produce());// Egg { }console.log(cow.produce());// Milk { }console.log(randomNumberGenerator.produce());//0.2626353555444987console.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 objectschicken,cow, andrandomNumberGenerator of their respective type.
• Lines 5–7 print for the previously created objects the respective results (provided as comments) when invokingproduce.
• Line 9 (resp. 10) demonstrates type safe use of the methodanimalToFood applied tochicken (resp.cow).
• Line 11, if uncommented, would result in a type error at compile time. Although theimplementation ofanimalToFood could invoke theproduce method ofrandomNumberGenerator, thetype annotation ofanimalToFood disallows it. This is in accordance with the intended meaning ofanimalToFood.
• Line 13 (resp. 15) demonstrates that applyinganimalToFood tochicken (resp.cow) results in an object of typeEgg (resp.Milk).
• Line 14 (resp. 16) demonstrates that applyinganimalToFood tocow (resp.chicken) does not result in an object of typeEgg (resp.Milk). Therefore, if uncommented, line 14 (resp. 16) would result in a type error at compile time.

The above minimalist example can be realized usinginheritance, for instance by deriving the classesChicken andCow from a base classAnimal.However, in a larger setting, this could be disadvantageous.Introducing new classes into a class hierarchy is not necessarily justified forcross-cutting concerns, or maybe outright impossible, for example when using an external library. Imaginably, the above example could be extended with the following classes:

• a classHorse that does not have aproduce method;
• a classSheep that has aproduce method returningWool;
• a classPig that has aproduce method, which can be used only once, returningMeat.

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.

The above minimalist example already shows thatduck typing is less suited to realize the given scenario.While the classRandomNumberGenerator contains aproduce method, the objectrandomNumberGenerator should not be a valid argument foranimalToFood.The above example can be realized using duck typing, for instance by introducing a new fieldargumentForAnimalToFood to the classesChicken andCow signifying that objects of corresponding type are valid arguments foranimalToFood.However, this would not only increase the size of the respective classes (especially with the introduction of more methods similar toanimalToFood), but is also a non-local approach with respect toanimalToFood.

The above example can be realized usingfunction overloading, for instance by implementing two methodsanimalToFood(animal:Chicken):Egg andanimalToFood(animal:Cow):Milk.In TypeScript, such a solution is almost identical to the provided example. Other programming languages, such asJava, require distinct implementations of the overloaded method.This may lead to eithercode duplication orboilerplate code.

The above example can be realized using thevisitor pattern.It would require each animal class to implement anaccept method accepting an object implementing the interfaceAnimalVisitor (adding non-localboilerplate code).The functionanimalToFood would be realized as thevisit method of an implementation ofAnimalVisitor.Unfortunately, the connection between the input type (Chicken orCow) and the result type (Egg orMilk) would be difficult to represent.

Parametric polymorphism is conceptually equivalent to infinite intersection types.^[7]

Intersection types have been promoted as being "compositional" in contrast with thelet-bound polymorphism of ML (a restricted form of parametric polymorphism) because intersection types haveprincipal typings while ML's type system does not (not to be confused with principal types, which ML does enjoy). The lack of principal typings in ML translates into the need to evaluate some expressions before others in an ML program; essentially resulting in a data dependency at type-inference level in ML, in particular inlet expressions.^[8] Consequently, intersection types have been proposed as a way to improveincremental compilation^[9] and/orgradual typing.^[10]

On the other hand, intersection types have been criticized for not being compositional in another sense, namely that in a putative system that uses only intersection types but has no parametric polymorphism, inferred may types depend on the local features of a module, which may compose badly with other modules unless whole program compilation happens at source level. As a trivial example, anidentity function that is exposed through a public interface, e.g. exported by a module, ideally is parametrically polymorphic, so that it can be used with future types that the writer (of that function) doesn't yet know about. However, in a system that only has intersection types, such a function would be inferred to intersect at best over types existing when it is compiled.^[11]

On the one hand, intersection typescan 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 approachrequires 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, orduck typing, then the verbose nature of intersection types is unfavorable.Therefore, intersection types should be considered complementary to existing specification methods.

Adependent intersection type, denoted${\displaystyle (x:\sigma )\cap \tau }$, is adependent type in which the type${\displaystyle \tau }$ may depend on the term variable${\displaystyle x}$.^[12]In particular, if a term${\displaystyle M}$ has the dependent intersection type${\displaystyle (x:\sigma )\cap \tau }$, then the term${\displaystyle M}$ hasboth the type${\displaystyle \sigma }$ and the type${\displaystyle \tau [x:=M]}$, where${\displaystyle \tau [x:=M]}$ is the type which results from replacing all occurrences of the term variable${\displaystyle x}$ in${\displaystyle \tau }$ by the term${\displaystyle M}$.

Scala supports type declarations^[13] as object members. This allows a type of an object member to depend on the value of another member, which is called apath-dependent type.^[14]For example, the following program text defines a Scala traitWitness, which can be used to implement thesingleton pattern.^[15]

traitWitness{typeTvalvalue:T{}}

The above traitWitness declares the memberT, which can be assigned atype as its value, and the membervalue, which can be assigned a value of typeT.The following program text defines an objectbooleanWitness as instance of the above traitWitness.The objectbooleanWitness defines the typeT asBoolean and the valuevalue astrue.For example, executingSystem.out.println(booleanWitness.value) printstrue on the console.

objectbooleanWitnessextendsWitness{typeT=Booleanvalvalue=true}

Let${\displaystyle ⟨\mathsf{\text{x}}:\sigma ⟩}$ be the type (specifically, arecord type) of objects having the member${\displaystyle \mathsf{\text{x}}}$ of type${\displaystyle \sigma }$.In the above example, the objectbooleanWitness can be assigned the dependent intersection type${\displaystyle (x:⟨\mathsf{\text{T}}:\text{Type}⟩)\cap ⟨\mathsf{\text{value}}:x.\mathsf{\text{T}}⟩}$.The reasoning is as follows. The objectbooleanWitness has the memberT that is assigned the typeBoolean as its value.SinceBoolean is a type, the objectbooleanWitness has the type${\displaystyle ⟨\mathsf{\text{T}}:\text{Type}⟩}$.Additionally, the objectbooleanWitness has the membervalue that is assigned the valuetrue of typeBoolean.Since the value ofbooleanWitness.T isBoolean, the objectbooleanWitness has the type${\displaystyle ⟨\mathsf{\text{value}}:\mathsf{\text{booleanWitness.T}}⟩}$.Overall, the objectbooleanWitness has the intersection type${\displaystyle ⟨\mathsf{\text{T}}:\text{Type}⟩\cap ⟨\mathsf{\text{value}}:\mathsf{\text{booleanWitness.T}}⟩}$.Therefore, presenting self-reference as dependency, the objectbooleanWitness has the dependent intersection type${\displaystyle (x:⟨\mathsf{\text{T}}:\text{Type}⟩)\cap ⟨\mathsf{\text{value}}:x.\mathsf{\text{T}}⟩}$.

Alternatively, the above minimalistic example can be described usingdependent record types.^[16]In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept.^[12]

Anintersection of a type family, denoted$\bigcap _{x:\sigma }\tau$, is adependent type in which the type${\displaystyle \tau }$ may depend on the term variable${\displaystyle x}$. In particular, if a term${\displaystyle M}$ has the type$\bigcap _{x:\sigma }\tau$, then foreach term${\displaystyle N}$ of type${\displaystyle \sigma }$, the term${\displaystyle M}$ has the type${\displaystyle \tau [x:=N]}$. This notion is also calledimplicitPi type,^[17] observing that the argument${\displaystyle N}$ is not kept at term level.

• Type theory
• Type systems
• Data types
• Composite data types
• Polymorphism (computer science)
• TypeScript

• Articles with short description
• Short description is different from Wikidata