Global InformationIntersection type information
| Type systems |
|---|
| General concepts |
|
| Major categories |
|
| Minor categories |
|
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.
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]
- ^ 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.
- ^ 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.
- ^ 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.