Union types

Polymorphic Type Inference for Dynamic Languages

Giuseppe Castagna, Mickaël Laurent & Kim Nguyen
We present a type system that combines, in a controlled way, first-order polymorphism with intersectiontypes, union types, and subtyping, and prove its safety. This makes the system a prime candidate to type dynamic languages.

On type-cases, union elimination, and occurrence typing

Giuseppe Castagna, Mickaël Laurent, Kim Nguyen & Matthew Lutze
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing.