In type theory, an **intersection type** can be allocated to values that can be assigned both the type and the type . This value can be given the intersection type 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`

.

- TypeScript example
- Comparison to inheritance
- Comparison to duck typing
- Comparison to function overloading
- Comparison to the visitor pattern
- Limitations
- Dependent intersection type
- Scala example
- Intersection of a type family
- Comparison of languages with intersection types
- References

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 `number=>number`

is the type of function taking a number as an argument and returning a number, and `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, 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 cross-cutting 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 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 `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.

`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 the ad hoc polymorphic 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 type `Egg`

, and when applied to an argument of type `Cow`

returns an object of type 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 milkletanimalToFood:((_: Chicken)=>Egg)&((_: Cow)=>Milk)=function(animal: any){returnanimal.produce();};`

Finally, the following program code demonstrates type 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 objects
`chicken`

,`cow`

, and`randomNumberGenerator`

of their respective type. - Lines 5–7 print for the previously created objects the respective results (provided as comments) when invoking
`produce`

. - Line 9 (resp. 10) demonstrates type safe use of the method
`animalToFood`

applied to`chicken`

(resp.`cow`

). - Line 11, if uncommitted, 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`

. - Line 13 (resp. 15) demonstrates that applying
`animalToFood`

to`chicken`

(resp.`cow`

) results in an object of type`Egg`

(resp.`Milk`

). - 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.

The above minimalist example can be realized using inheritance, 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 cross-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 class
`Horse`

that does not have a`produce`

method; - a class
`Sheep`

that has a`produce`

method returning`Wool`

; - a class
`Pig`

that has a`produce`

method, which can be used only once, returning`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.

The above minimalist example already shows that duck typing 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`

.

The above example can be realized using function overloading, 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 Java, require distinct implementations of the overloaded method. This may lead to either code duplication or boilerplate code.

The above example can be realized using the visitor pattern. It would require each animal class to implement an `accept`

method accepting an object implementing the interface `AnimalVisitor`

(adding non-local boilerplate code). 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.

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.

A **dependent intersection type**, denoted , is a dependent type in which the type may depend on the term variable .^{ [6] } In particular, if a term has the dependent intersection type , then the term has *both* the type and the type , where is the type which results from replacing all occurrences of the term variable in by the term .

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 *path-dependent type*.^{ [8] } For example, the following program text defines a Scala trait `Witness`

, which can be used to implement the singleton pattern.^{ [9] }

`traitWitness{typeTvalvalue: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 programm 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.

`objectbooleanWitnessextendsWitness{typeT=Booleanvalvalue=true}`

Let be the type (specifically, a record type) of objects having the member of type . In the above example, the object `booleanWitness`

can be assigned the dependent intersection type . 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 . 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 . Overall, the object `booleanWitness`

has the intersection type . Therefore, presenting self-reference as dependency, the object `booleanWitness`

has the dependent intersection type .

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] }

An **intersection of a type family**, denoted , is a dependent type in which the type may depend on the term variable .^{ [6] } In particular, if a term has the type , then for *each* term of type , the term has the type . This notion is also called *implicit Pi type *,^{ [11] } observing that the argument is not kept at term level.

Language | Actively developed | Paradigm(s) | Status | Features |
---|---|---|---|---|

C# | Yes^{ [12] } | Under discussion^{ [13] } | ? | |

Ceylon | Yes^{ [14] } | Supported^{ [15] } | - Type refinement
- Interface composition
- Subtyping in width
| |

F# | Yes^{ [16] } | Under discussion^{ [17] } | ? | |

Flow | Yes^{ [18] } | Supported^{ [19] } | - Type refinement
- Interface composition
| |

Forsythe | No | Supported^{ [20] } | - Function type intersection
- Distributive, co- and contravariant function type subtyping
| |

Java | Yes^{ [21] } | Supported^{ [22] } | - Type refinement
- Interface composition
- Subtyping in width
| |

Scala | Yes^{ [23] } | Supported^{ [24] }^{ [25] } | - Type refinement
- Trait composition
- Subtyping in width
| |

TypeScript | Yes^{ [26] } | Supported^{ [5] } | - Arbitrary type intersection
- Interface composition
- Subtyping in width and depth
| |

Whiley | Yes^{ [27] } | Supported^{ [28] } | ? |

In mechanics, the **virial theorem** provides a general equation that relates the average over time of the total kinetic energy of a stable system of discrete particles, bound by potential forces, with that of the total potential energy of the system. Mathematically, the theorem states

In mathematics, **open sets** are a generalization of open intervals in the real line. In a metric space—that is, when a distance is defined—open sets are the sets that, with every point P, contain all points that are sufficiently near to P.

In mathematics, logic, and computer science, a **type system** is a formal system in which every term has a "type" which defines its meaning and the operations that may be performed on it. **Type theory** is the academic study of type systems.

In physics, a **Langevin equation** is a stochastic differential equation describing the time evolution of a subset of the degrees of freedom. These degrees of freedom typically are collective (macroscopic) variables changing only slowly in comparison to the other (microscopic) variables of the system. The fast (microscopic) variables are responsible for the stochastic nature of the Langevin equation. One application is to Brownian motion, calculating the statistics of the random motion of a small particle in a fluid due to collisions with the surrounding molecules in thermal motion.

In programming languages, a **type system** is a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program, such as variables, expressions, functions or modules. These types formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components. The main purpose of a type system is to reduce possibilities for bugs in computer programs by defining interfaces between different parts of a computer program, and then checking that the parts have been connected in a consistent way. This checking can happen statically, dynamically, or as a combination of both. Type systems have other purposes as well, such as expressing business rules, enabling certain compiler optimizations, allowing for multiple dispatch, providing a form of documentation, etc.

In mathematics, the **covariant derivative** is a way of specifying a derivative along tangent vectors of a manifold. Alternatively, the covariant derivative is a way of introducing and working with a connection on a manifold by means of a differential operator, to be contrasted with the approach given by a principal connection on the frame bundle – see affine connection. In the special case of a manifold isometrically embedded into a higher-dimensional Euclidean space, the covariant derivative can be viewed as the orthogonal projection of the Euclidean directional derivative onto the manifold's tangent space. In this case the Euclidean derivative is broken into two parts, the extrinsic normal component and the intrinsic covariant derivative component.

The **Drude model** of electrical conduction was proposed in 1900 by Paul Drude to explain the transport properties of electrons in materials. The model, which is an application of kinetic theory, assumes that the microscopic behaviour of electrons in a solid may be treated classically and looks much like a pinball machine, with a sea of constantly jittering electrons bouncing and re-bouncing off heavier, relatively immobile positive ions.

The **adiabatic theorem** is a concept in quantum mechanics. Its original form, due to Max Born and Vladimir Fock (1928), was stated as follows:

In mathematics, a **field of sets** is a mathematical structure consisting of a pair where is a set and is a family of subsets of called an **algebra over ** that contains the empty set as an element, and is closed under the operations of taking complements in , finite unions, and finite intersections. Equivalently, an algebra over is a subset of the power set of such that

- for all
- , and
- for all

In probability theory and statistics, given a stochastic process, the **autocovariance** is a function that gives the covariance of the process with itself at pairs of time points. Autocovariance is closely related to the autocorrelation of the process in question.

The **simply typed lambda calculus**, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.

In mathematics, the **Fréchet derivative** is a derivative defined on Banach spaces. Named after Maurice Fréchet, it is commonly used to generalize the derivative of a real-valued function of a single real variable to the case of a vector-valued function of multiple real variables, and to define the functional derivative used widely in the calculus of variations.

In the statistical mechanics of quantum mechanical systems and quantum field theory, the properties of a system in thermal equilibrium can be described by a mathematical object called a **Kubo–Martin–Schwinger state** or, more commonly, a **KMS state**: a state satisfying the **KMS condition**. Kubo (1957) introduced the condition, Martin & Schwinger (1959) used it to define thermodynamic Green's functions, and Rudolf Haag, M. Winnink, and N. M. Hugenholtz (1967) used the condition to define equilibrium states and called it the KMS condition.

In logic, a **modal companion** of a superintuitionistic (intermediate) logic *L* is a normal modal logic that interprets *L* by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

In many-body theory, the term **Green's function** is sometimes used interchangeably with correlation function, but refers specifically to correlators of field operators or creation and annihilation operators.

**Resonance fluorescence** is the process in which a two-level atom system interacts with the quantum electromagnetic field if the field is driven at a frequency near to the natural frequency of the atom.

**Photon antibunching** generally refers to a light field with photons more equally spaced than a coherent laser field, a signature being signals at appropriate detectors which are anticorrelated. More specifically, it can refer to sub-Poissonian photon statistics, that is a photon number distribution for which the variance is less than the mean. A coherent state, as output by a laser far above threshold, has Poissonian statistics yielding random photon spacing; while a thermal light field has super-Poissonian statistics and yields bunched photon spacing. In the thermal (bunched) case, the number of fluctuations is larger than a coherent state; for an antibunched source they are smaller.

In mathematical logic, category theory, and computer science, **kappa calculus** is a formal system for defining first-order functions.

In type theory a **typing environment** represents the association between variable names and data types.

**Tau functions** are an important ingredient in the modern theory of integrable systems, and have numerous applications in a variety of other domains. They were originally introduced by **Ryogo Hirota** in his *direct method* approach to soliton equations, based on expressing them in an equivalent bilinear form. The term **Tau function**, or **-function**, was first used systematically by Mikio Sato and his students in the specific context of the Kadomtsev–Petviashvili equation, and related integrable hierarchies. It is a central ingredient in the theory of solitons. Tau functions also appear as matrix model partition functions in the spectral theory of Random Matrices, and may also serve as generating functions, in the sense of combinatorics and enumerative geometry, especially in relation to moduli spaces of Riemann surfaces, and enumeration of branched coverings, or so-called Hurwitz numbers.

- ↑ 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. - ↑ Palsberg, Jens (2012). "Overloading is NP-Complete".
*Logic and Program Semantics*. Lecture Notes in Computer Science.**7230**. pp. 204–218. doi:10.1007/978-3-642-29485-3_13. ISBN 978-3-642-29484-6. - ↑ Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013).
*Lambda Calculus with Types*. Cambridge University Press. pp. 1–. ISBN 978-0-521-76614-2. - ↑ 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 . - 1 2 "Intersection Types in TypeScript" . Retrieved 2019-08-01.
- 1 2 3 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. - ↑ "Type declarations in Scala" . Retrieved 2019-08-15.
- ↑ 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 - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday*.*Lecture Notes in Computer Science*.**9600**. Springer. pp. 249–272. doi:10.1007/978-3-319-30936-1_14. - ↑ "Singletons in the Scala shapeless library" . Retrieved 2019-08-15.
- ↑ 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. - ↑ 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" . Retrieved 2019-08-08.
- ↑ "Discussion: Union and Intersection types in C Sharp" . Retrieved 2019-08-08.
- ↑ "Eclipse Ceylon: Welcom to Ceylon" . Retrieved 2019-08-08.
- ↑ "Intersection Types in Ceylon" . Retrieved 2019-08-08.
- ↑ "F# Software Foundation" . Retrieved 2019-08-08.
- ↑ "Add Intersection Types to F Sharp" . Retrieved 2019-08-08.
- ↑ "Flow: A Static Type Checker for JavaScript" . Retrieved 2019-08-08.
- ↑ "Intersection Type Syntax in Flow" . Retrieved 2019-08-08.
- ↑ Reynolds, J. C. (1988). Preliminary design of the programming language Forsythe.
- ↑ "Java Software" . Retrieved 2019-08-08.
- ↑ "IntersectionType (Java SE 12 & JDK 12)" . Retrieved 2019-08-01.
- ↑ "The Scala Programming Language" . Retrieved 2019-08-08.
- ↑ "Compound Types in Scala" . Retrieved 2019-08-01.
- ↑ "Intersection Types in Dotty" . Retrieved 2019-08-01.
- ↑ "TypeScript - JavaScript that scales" . Retrieved 2019-08-01.
- ↑ "Whiley: an Open Source Programming Language with Extended Static Checking" . Retrieved 2019-08-01.
- ↑ "Whiley language specification" (PDF). Retrieved 2019-08-01.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.