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.
Reader’s guide
This paper is a distilled overview of Chapter 5 of my dissertation.
@InProceedings{Dunfield11:letnormal,
author = {Joshua Dunfield},
title = {Untangling Typechecking of Intersections and Unions},
booktitle = {Proceedings of the Workshop on Intersection
Types and Related Systems (ITRS '10)},
series = {EPTCS},
volume = {45},
year = {2011},
pages = {59--70},
note = {\url{arXiv:1101.4428 [cs.PL]}}
}
@Unpublished{Dunfield10:letnormal-preliminary,
author = {Joshua Dunfield},
title = {Untangling Typechecking of Intersections and Unions},
booktitle = {Preliminary proceedings of the Workshop on Intersection
Types and Related Systems (ITRS '10)},
month = jul,
year = {2010},
note = {\url{http://www.cs.cmu.edu/~joshuad/papers/letnormal}}
}