We present a type system that combines, in a controlled way, first-order polymorphism with intersectiontypes, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that issound and terminating. This yields a system in which unannotated functions are given polymorphic types(thanks to Hindley-Milner) that can express the overloaded behavior of the functions they type (thanks tothe intersection introduction rule) and that are deduced by applying advanced techniques of type narrowing(thanks to the union elimination rule). This makes the system a prime candidate to type dynamic languages.

翻译：我们提出了一种以受控方式将一阶多态性与交集类型、并集类型及子类型相结合的型系统，并证明其安全性。随后定义了一种具有可靠性和终止性的类型重构算法。由此生成的系统能够为无标注函数赋予多态类型（得益于Hindley-Milner系统），这些类型既能表达被类型化函数的重载行为（得益于交集引入规则），又能通过应用先进的类型窄化技术进行推导（得益于并集消去规则）。这使得该系统成为动态语言类型化的理想候选方案。