Typecases

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.

Giuseppe Castagna, Victor Lanvin, Mickaël Laurent & Kim Nguyen
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages.