一句话：提出线性约束，把隐式线性参数作为限定类型，扩展 GHC 约束求解器自动推断，降低 Linear Haskell 使用负担。
线性类型可确保文件句柄、手动管理内存等资源被安全使用：线性参数必须在其函数体中被恰好消费一次。然而，显式书写线性参数会带来大量样板与官僚式负担。本文提出 linear constraints（线性约束），一种面向线性类型的前端特性：它们是隐式线性参数，由编译器自动填充。作者将线性约束形式化为一种 qualified type system（限定类型系统），并给出推断算法，该算法扩展了 GHC 现有的约束求解器。其可靠性（soundness）通过将线性约束脱糖（desugar）为 Linear Haskell 得到保证。该工作以 GHC/Linear Haskell 为背景，旨在让能力（capabilities）与唯一性（uniqueness）等资源使用更易表达，同时保持线性类型的安全性。
A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. This paper presents linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are filled in automatically by the compiler. We present linear constraints as a qualified type system,together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.
@article{paperbot1489,
title = {Linearly qualified types: generic inference for capabilities and uniqueness},
author = {Arnaud Spiwack and Csongor Kiss and Jean-Philippe Bernardy and Nicolas Wu and Richard A. Eisenberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547626}
}