About: Intersection type discipline

In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor to assign multiple types to a single term.In particular, if a term can be assigned both' the type and the type , then can be assigned the intersection type (and vice versa).Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism (as opposed to parametric polymorphism).For example, the λ-term can be assigned the type in most intersection type systems, assuming for the term variable both the function type and the corresponding argument type .