Intersection type explained

In type theory, an intersection type can be allocated to values that can be assigned both the type

\sigma

and the type

\tau

. This value can be given the intersection type

\sigma\cap\tau

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 implements both the and the interfaces. Therefore, an object of type can be safely passed to functions expecting an argument of type and to functions expecting an argument of type .

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

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

The following program code defines the classes,, and that each have a method returning an object of either type,, or .Additionally, the functions and require arguments of type and, respectively.

class Egg class Milk

// produces eggsclass Chicken

// produces milkclass Cow

// produces a random numberclass RandomNumberGenerator

// requires an eggfunction eatEgg(egg: Egg)

// requires milkfunction drinkMilk(milk: Milk)

The following program code defines the ad hoc polymorphic function that invokes the member function of the given object .The function has two type annotations, namely and, connected via the intersection type constructor .Specifically, when applied to an argument of type returns an object of type type, and when applied to an argument of type returns an object of type type .Ideally, should not be applicable to any object having (possibly by chance) a method.// given a chicken, produces an egg; given a cow, produces milklet animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) = function (animal: any) ;

Finally, the following program code demonstrates type safe 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:

Comparison to inheritance

The above minimalist example can be realized using inheritance, for instance by deriving the classes and from a base class .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:

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 is less suited to realize the given scenario.While the class contains a method, the object should not be a valid argument for .The above example can be realized using duck typing, for instance by introducing a new field to the classes and signifying that objects of corresponding type are valid arguments for .However, this would not only increase the size of the respective classes (especially with the introduction of more methods similar to), but is also a non-local approach with respect to .

Comparison to function overloading

The above example can be realized using function overloading, for instance by implementing two methods and .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.

Comparison to the visitor pattern

The above example can be realized using the visitor pattern.It would require each animal class to implement an method accepting an object implementing the interface (adding non-local boilerplate code).The function would be realized as the method of an implementation of .Unfortunately, the connection between the input type (or) and the result type (or) 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, or 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

(x:\sigma)\cap\tau

, is a dependent type in which the type

\tau

may depend on the term variable

x

.[5] In particular, if a term

M

has the dependent intersection type

(x:\sigma)\cap\tau

, then the term

M

has both the type

\sigma

and the type

\tau[x:=M]

, where

\tau[x:=M]

is the type which results from replacing all occurrences of the term variable

x

in

\tau

by the term

M

.

Scala example

Scala supports type declarations [6] 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.[7] For example, the following program text defines a Scala trait Witness, which can be used to implement the singleton pattern.[8] trait Witness 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

Let

\langlesf{x}:\sigma\rangle

be the type (specifically, a record type) of objects having the member

sf{x}

of type

\sigma

.In the above example, the object booleanWitness can be assigned the dependent intersection type

(x:\langlesf{T}:Type\rangle)\cap\langlesf{value}:x.sf{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

\langlesf{T}: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

\langlesf{value}:sf{booleanWitness.T}\rangle

.Overall, the object booleanWitness has the intersection type

\langlesf{T}:Type\rangle\cap\langlesf{value}:sf{booleanWitness.T}\rangle

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

(x:\langlesf{T}:Type\rangle)\cap\langlesf{value}:x.sf{T}\rangle

.

Alternatively, the above minimalistic example can be described using dependent record types.[9] In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept.[5]

Intersection of a type family

An intersection of a type family, denoted \bigcap_ \tau, is a dependent type in which the type

\tau

may depend on the term variable

x

. In particular, if a term

M

has the type \bigcap_ \tau, then for each term

N

of type

\sigma

, the term

M

has the type

\tau[x:=N]

. This notion is also called implicit Pi type,[10] observing that the argument

N

is not kept at term level.

Comparison of languages with intersection types

Language Actively developed Paradigm(s) Status Features
[11] [12] 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.
[13] [14]
  • Type refinement
  • Interface composition
  • Subtyping in width
[15] [16]
Flow [17] [18]
  • Type refinement
  • Interface composition
[19]
  • Function type intersection
  • Distributive, co- and contravariant function type subtyping
[20] [21]
  • Type refinement
  • Interface composition
  • Subtyping in width
[22] [23]
  • Type refinement
  • Interface composition
[24] [25] [26]
  • Type refinement
  • Trait composition
  • Subtyping in width
[27] [28]
  • Arbitrary type intersection
  • Interface composition
  • Subtyping in width and depth
[29] [30]

Notes and References

  1. 10.2307/2273659 . 2273659 . A filter lambda model and the completeness of type assignment . Journal of Symbolic Logic . 48 . 4 . 931–940 . 1983 . Barendregt . Henk . Coppo . Mario . Dezani-Ciancaglini . Mariangiola. 45660117 . Mariangiola Dezani-Ciancaglini .
  2. Book: 10.1007/978-3-642-29485-3_13 . Overloading is NP-Complete . Logic and Program Semantics . 7230 . 204–218 . Lecture Notes in Computer Science . 2012 . Palsberg . Jens . 978-3-642-29484-6 .
  3. Book: Henk Barendregt. Wil Dekkers. Richard Statman. Lambda Calculus with Types. 20 June 2013. Cambridge University Press. 978-0-521-76614-2. 1–.
  4. 10.1305/ndjfl/1040067315 . Strong normalization and typability with intersection types . Notre Dame Journal of Formal Logic . 37 . 1 . 44–52 . 1996 . Ghilezan . Silvia . free .
  5. Dependent intersection: A new way of defining records in type theory . Kopylov . Alexei . 2003 . IEEE Computer Society . 18th IEEE Symposium on Logic in Computer Science . 86–95 . LICS 2003 . 10.1109/LICS.2003.1210048 . 10.1.1.89.4223 .
  6. Web site: Type declarations in Scala . 2019-08-15.
  7. Book: Amin . Nada . Grütter . Samuel . Odersky . Martin . Rompf . Tiark . Stucki . Sandro . A List of Successes That Can Change the World . The Essence of Dependent Object Types . Lecture Notes in Computer Science . 9600 . 249–272 . 2016 . Springer . 10.1007/978-3-319-30936-1_14 . 978-3-319-30935-4 .
  8. Web site: Singletons in the Scala shapeless library . . 2019-08-15.
  9. Dependently typed records for representing mathematical structure . Pollack . Robert . Springer . Theorem Proving in Higher Order Logics, 13th International Conference . 462–479 . TPHOLs 2000 . 2000 . 10.1007/3-540-44659-1_29 .
  10. Stump . Aaron . 2018 . From realizability to induction via dependent intersection . Annals of Pure and Applied Logic . 169 . 7 . 637–655 . 10.1016/j.apal.2018.03.002 . free .
  11. Web site: C# Guide . 2019-08-08.
  12. Web site: Discussion: Union and Intersection types in C Sharp . . 2019-08-08.
  13. Web site: Eclipse Ceylon™. 19 July 2017 . 2023-08-16.
  14. Web site: Intersection Types in Ceylon . 19 July 2017 . 2019-08-08.
  15. Web site: F# Software Foundation . 2019-08-08.
  16. Web site: Add Intersection Types to F Sharp . . 2019-08-08.
  17. Web site: Flow: A Static Type Checker for JavaScript. 2019-08-08.
  18. Web site: Intersection Type Syntax in Flow . 2019-08-08.
  19. Reynolds, J. C. (1988). Preliminary design of the programming language Forsythe.
  20. Web site: Java Software . 2019-08-08.
  21. Web site: IntersectionType (Java SE 12 & JDK 12) . 2019-08-01.
  22. Web site: php.net.
  23. Web site: PHP.Watch - PHP 8.1: Intersection Types.
  24. Web site: The Scala Programming Language. 2019-08-08.
  25. Web site: Compound Types in Scala . 2019-08-01.
  26. Web site: Intersection Types in Dotty . 2019-08-01.
  27. Web site: TypeScript - JavaScript that scales. . 2019-08-01.
  28. Web site: Intersection Types in TypeScript . 2019-08-01.
  29. Web site: Whiley: an Open Source Programming Language with Extended Static Checking . 2019-08-01.
  30. Web site: Whiley language specification . 2019-08-01.