Untangling Typechecking of Intersections and Unions

Joshua Dunfield

Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics.

Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program.

In Elaine Pimentel, Betti Venneri and Joe Wells: Proceedings Fifth Workshop on Intersection Types and Related Systems (ITRS 2010), Edinburgh, U.K., 9th July 2010, Electronic Proceedings in Theoretical Computer Science 45, pp. 59–70.
Published: 21st January 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.45.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org