2011/01/24 by Jana Dunfield
Computer Science · #cs.PL
paper · pdf · doi:10.4204/eptcs.45.5
published as EPTCS 45, 2011, pp. 59-70 · In Proceedings ITRS 2010, arXiv:1101.4104
arxiv created 2011/01/24 · arxiv updated 2021/03/24
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.