线性合格类型：能力和唯一性的通用推断
摘要：线性参数在其函数体中必须被消耗一次。 当将资源（如文件句柄和手动管理的内存）声明为线性参数时，线性类型系统可以验证这些资源的安全使用。然而，使用显式线性参数编写代码需要繁文缛节。本文介绍了线性约束（linear constraints）作为一种前端特性，用于减少使用线性类型时的繁文缛节。线性约束是由编译器自动填充的隐式线性参数。我们将线性约束作为一个限定类型系统（qualified type system），并提出了一个推理算法，该算法扩展了 GHC 的现有约束求解算法。线性约束的可靠性由它们被转化为线性 Haskell 保证。
作者：Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard Eisenberg
论文ID：2103.06127
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-25