一句话：系统研究数据类型声明的 kind 推断，为 Haskell98 与 PolyKinds 给出声明式及算法化规范并证明其性质。
随着 Haskell 等语言不断引入显著增强类型系统表达力的新特性，数据类型声明中的 kind 推断已成为独立且重要的研究问题。本文研究数据类型的 kind 推断，受类型推断研究启发，分别为 Haskell98 和基于现代 Haskell 扩展（含有限形式依赖类型）的 PolyKinds 系统给出声明式规范，界定哪些数据类型声明应被接受。作者认为这些形式化表述即使对 Haskell98 也是新颖且此前未有的。文章进一步给出可实现算法化版本，并研究这些系统的可靠性、完备性以及主 kind 的存在性，在性质成立处给出证明。该工作可为希望形式化数据类型声明的语言设计者，以及寻求有原则地主 kind 推断的实现者提供指南。
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own. This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a more advanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form of dependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These specifications are complemented with implementable algorithmic versions. We study soundness, completeness and the existence of principal kinds in these systems, proving the properties where they hold. This work can serve as a guide both to language designers who wish to formalize their datatype declarations and also to implementors keen to have principled inference of principal types.
@article{paperbot571,
title = {Kind inference for datatypes},
author = {Ningning Xie and Richard A. Eisenberg and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371121}
}