一句话：为 Boolean-kinded Hindley-Milner 扩展给出等式泛化与半统一算法，支持 let 泛化和多态递归，并最小化布尔类型变量。
将 Hindley-Milner（HM）类型系统扩展为 Boolean kinds 后可支持多种特性的类型推断，但局部 let 泛化与多态递归等经典机制在此类扩展中要么受限要么未知。本文针对这一问题，提出在任意布尔环中进行等式泛化（equational generalization）与半统一（semiunification）的过程，从而在 Boolean-kinded 类型推断中实现 let 泛化与多态递归。此外，作者开发了最小化受限布尔类型变量数量的方法，以保持这些系统中的类型表示紧凑。论文以可空引用类型（nullable reference types）作为 Boolean-kinded HM 扩展的实例，并说明如何利用所提出的过程来支持 let 泛化与多态递归。
Recent research has demonstrated the effectiveness of extending the Hindley-Milner (HM) type system with Boolean kinds to support type inference for a wide variety of features. However, the means to support classic type system provisions such as local let generalization and polymorphic recursion is either limited or unknown for such extensions. This paper contributes procedures for equational generalization and semiunification in arbitrary Boolean rings, enabling let generalization and polymorphic recursion in Boolean-kinded type inference. Additionally, methods to minimize the number of bound Boolean type variables are developed to keep types small in these systems. Boolean-kinded HM extensions are exemplified with nullable reference types , and how to use the developed procedures to support let generalization and polymorphic recursion is outlined.
@article{Zullo26,
title = {Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems},
author = {Joseph A. Zullo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776644}
}