Untangling Typechecking of Intersections and Unions

TL;DR

This paper addresses the challenges of typechecking union types in programming languages by proposing a case-analysis technique within bidirectional typechecking, and demonstrates that program normalization preserves soundness and completeness.

Contribution

It introduces a method for typechecking union types using case analysis and program normalization, ensuring soundness and completeness in a call-by-value setting.

Findings

Case analysis technique preserves soundness.

Let-normal form reduces complexity of typechecking.

Soundness and completeness are maintained after normalization.

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.