Intersection type

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

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. 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. 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. Remarkably, program termination can be precisely characterized using intersection types. Consequently, type inference for infinite-intersection types is undecidable, but it is decidable for all finite rank intersection types. class Egg { private kind: "Egg"; } class Milk { private kind: "Milk"; } // "Produces" a product interface Producer { produce(): T; } // produces eggs class Chicken implements Producer { produce(): Egg { return new Egg(); } } // produces milk class Cow implements Producer { produce(): Milk { return new Milk(); } } // produces a random number class RandomNumberGenerator implements Producer { produce(): number { return Math.random(); } } // requires an egg function eatEgg(egg: Egg): string { return "I ate an egg."; } // requires milk function drinkMilk(milk: Milk): string { return "I drank some 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 , and when applied to an argument of type returns an object of 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 milk const animalToFood: ((animal: Chicken) => Egg) & ((animal: Cow) => Milk) = (animal: any) => { return animal.produce(); }; Finally, the following program code demonstrates type safe use of the above definitions. let chicken: Chicken = new Chicken(); let cow: Cow = new Cow(); let randomNumberGenerator: 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: Lines 1–3 create objects , , and of their respective type. Lines 5–7 print for the previously created objects the respective results (provided as comments) when invoking . Line 9 (resp. 10) demonstrates type safe use of the method applied to (resp. ). Line 11, if uncommented, would result in a type error at compile time. Although the implementation of could invoke the method of , the type annotation of disallows it. This is in accordance with the intended meaning of . Line 13 (resp. 15) demonstrates that applying to (resp. ) results in an object of type (resp. ). Line 14 (resp. 16) demonstrates that applying to (resp. ) does not result in an object of type (resp. ). Therefore, if uncommented, line 14 (resp. 16) would result in a type error at compile time. 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 . For example, the following program text defines a Scala trait Witness , which can be used to implement the singleton pattern. 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 \langle \textsf{x} : \sigma \rangle be the type (specifically, a record type) of objects having the member \textsf{x} of type \sigma . In the above example, the object booleanWitness can be assigned the dependent intersection type (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 \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 \langle \textsf{value} : \textsf{booleanWitness.T} \rangle . Overall, the object booleanWitness has the intersection type \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 : \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. In comparison to dependent intersection types, dependent record types constitute a strictly more specialized type theoretic concept. An intersection of a type family, denoted \bigcap_{x : \sigma} \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_{x : \sigma} \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, observing that the argument N is not kept at term level. ==References==

Text derived from https://en.wikipedia.org/w/index.php?oldid=1374885617 under CC BY-SA 4.0; modifications have been made.