Untangling typechecking of intersections and unions
ITRS '10 (Edinburgh, July 2010);
post-proceedings in
EPTCS 45,
arXiv:1101.4428 [cs.PL]
Abstract
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.
|
Version published in EPTCS 45 (proceedings of ITRS '10)
Version of June 2010 (pre-proceedings of ITRS '10)
BibTeX entry
@InProceedings{Dunfield11:letnormal,
author = {Jana 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 = {Jana 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.queensu.ca/~jana/papers/letnormal}}
}
J. Dunfield