一句话：提出直接作用于源类型的交/并/函数子类型算法，基于 duotyping 与可分裂类型，可判定且实现简洁。
交类型和并类型在现代编程语言中很常见；从逻辑看，子类型问题等价于判定逻辑蕴涵，但同时处理交、并、蕴含及分配律的算法非常复杂。本文提出一种新的子类型（与逻辑蕴涵）算法，直接作用于源类型，无需先做范式化。核心基于两个近期思想：以语言构造对偶性为基础的 duotyping，以及可分裂类型（splittable types），即能分解为两个更简单类型的类型。作者证明该算法相对于基于最小相关逻辑 B+ 的声明式子类型定义是可靠、完备且可判定的，并用不到 50 行函数式代码实现了该算法。
Subtyping with intersection and union types is nowadays common in many programming languages. From the perspective of logic, the subtyping problem is essentially the problem of determining logical entailment : does a logical statement follow from another one? Unfortunately, algorithms for deciding subtyping and logical entailment with intersections, unions and various distributivity laws can be highly non-trivial. This functional pearl presents a novel algorithmic formulation for subtyping (and logical entailment) in the presence of various distributivity rules between intersections, unions and implications (i.e. function types). Unlike many existing algorithms which first normalize types and then apply a subtyping algorithm on the normalized types, our new subtyping algorithm works directly on source types. Our algorithm is based on two recent ideas: a generalization of subtyping based on the duality of language constructs called duotyping ; and splittable types , which characterize types that decompose into two simpler types. We show that our algorithm is sound, complete and decidable with respect to a declarative formulation of subtyping based on the minimal relevant logic B + . Moreover, it leads to a simple and compact implementation in under 50 lines of functional code.
@article{paperbot1110,
title = {Distributing intersection and union types with splits and duality (functional pearl)},
author = {Xuejing Huang and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473594}
}