Intersection type

TypeScript supports intersection types, Intersection types have been promoted as being "compositional" in contrast with the let-bound polymorphism of ML (a restricted form of parametric polymorphism) because intersection types have principal 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 in let expressions. Consequently, intersection types have been proposed as a way to improve incremental compilation and/or gradual typing. 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 types may 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, an identity 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. 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. 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 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. 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. == Intersection of a type family ==

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. == Comparison of languages with intersection types ==