交和并的分类检查
Untangling Typechecking of Intersections and Unions
摘要：
交集和并集类型表示属性的合取和析取。使用双向类型检查，交集类型相对简单，但联合类型存在挑战。对于联合类型，我们可以在联合类型的子项出现在求值位置时进行案例分析（用变量替换子项，并在适当的假设下检查该项两次）。这种技术保留了按值调用语义的可靠性。可悲的是，有太多的子项选择，直接实现是不切实际的。但是仔细地将程序转换成let-范式会大大减少选择的数量。关键的结果是可靠性和完整性：一个类型派生（在系统中有太多的子项选择）存在的程序，当且仅当派生存在的let规范化的程序。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
