一句话：提出 MLstruct，在结构记录、等递归类型与一阶并/交类型下实现主多态类型推断。
并集与交集类型在 TypeScript 和 Scala 3 等语言中日益主流，但既有语言尚未将这类表达力强的类型与主多态类型推断结合起来。MLstruct 针对该问题，设计了一门支持子类型记录、等递归类型、一阶并集/交集、基于类的实例匹配以及 ML 风格主类型推断的语言。它整体上是结构类型，同时为类引入名义性，从而获得良好语义，并能表达一种无需 row variables 的可扩展变体。技术上，作者用合取、析取和否定连接词定义语言构造，保证其构成布尔代数，并添加少量非标准但可靠的子类型规则，以此获得足够结构来推导可靠且完备的类型推断算法，旨在推动未来语言拥有更好的类型推断。
Intersection and union types are becoming more popular by the day, entering the mainstream in programming languages like TypeScript and Scala 3. Yet, no language so far has managed to combine these powerful types with principal polymorphic type inference. We present a solution to this problem in MLstruct, a language with subtyped records, equirecursive types, first-class unions and intersections, class-based instance matching, and ML-style principal type inference. While MLstruct is mostly structurally typed, it contains a healthy sprinkle of nominality for classes, which gives it desirable semantics, enabling the expression of a powerful form of extensible variants that does not need row variables. Technically, we define the constructs of our language using conjunction, disjunction, and negation connectives, making sure they form a Boolean algebra, and we show that the addition of a few nonstandard but sound subtyping rules gives us enough structure to derive a sound and complete type inference algorithm. With this work, we hope to foster the development of better type inference for present and future programming languages with expressive subtyping systems.
@article{paperbot1436,
title = {MLstruct: principal type inference in a Boolean algebra of structural types},
author = {Lionel Parreaux and Chun Yin Chau},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563304}
}