Intersection types are types of the form which contain those values that are both of type and of type . Given such a value, it can be used as either one of the types:
Languages differ in how intersection types may be constructed. The first style is that an expression has type if it has both types, possibly by separate derivations:
The second style is to use subtyping, and define as a meet in the subtyping order, so that:
In this style, an expression can be given type by first typechecking it with some type which is a subtype of both, and then using the above rule and subtyping to give it type .
The crucial difference is that in the first style, the two typing derivations for and may be entirely different. This brings surprising complexity: for instance, in both the Coppo-Dezani1 and Barendregt-Coppo-Dezani2 systems (both simply typed lambda calculi with intersection types), type checking is undecidable as a term is typeable iff its execution terminates!
The counterexample here, however, is about the interaction between these types and mutability, a phenomenon pointed out by Davies and Pfenning3. First, a naive implementation of ML-style references is unsound:
(* Counterexample by Rowan Davies and Frank Pfenning *) (* Suppose we have types nat and pos, where nat is nonnegative integers and pos is its subtype of positive integers *) let x : nat ref ∧ pos ref = ref 1 in let () = (x := 0) in (* typechecks: x is a nat ref *) let z : pos = !x in (* typechecks: x is a pos ref *) z : pos (* now we have the positive number zero *)
Despite the lack of the symbol, this is essentially the same problem as in Polymorphic references: the same single reference is used at two different types. The same solutions apply, in particular, the value restriction.
However, there is a further potential source of unsoundness. In many systems with subtyping and intersection types, it is conventional to have:
That is, a value which is both a function that returns and a function that returns must be a function which returns values that are both and .
Even in the presence of the value restriction, type systems with intersection types and the above rule are unsound:
(* Counterexample by Rowan Davies and Frank Pfenning *) let f : (unit → nat ref) ∧ (unit → pos ref) = fun () → ref 1 in (* passes the value restriction *) let f' : unit → (nat ref ∧ pos ref) = f in (* uses the above rule *) let x : nat ref ∧ pos ref = f () let () = (x := 0) in let z : pos = !x in z : pos (* same problem as before *)
Note that both of these counterexamples rely on the first style of intersection types above, where intersections can be introduced with two different typing derivations. They do not arise if intersections are available only through subtyping, as in the second style.
An extension of the basic functionality theory for the λ-calculus, M. Coppo and M. Dezani-Ciancaglini (1980)
A filter lambda model and the completeness of type assignment, Barendregt, Coppo and Dezani-Ciancaglini (1983)
Intersection Types and Computational Effects, Rowan Davies and Frank Pfenning (2000)