Linear constraints are the linear counterpart of Haskell's class constraints. Linearly typed parameters allow the programmer to control resources such as file handles and manually managed memory as linear arguments. Indeed, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. Linear constraints address this shortcoming: a linear constraint acts as an implicit linear argument that can be filled in automatically by the compiler. We present this new feature 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. This paper is a revised and extended version of a previous paper by the same authors (arXiv:2103.06127). The formal system and the constraint solver have been significantly simplified and numerous additional applications are described.

翻译：线性约束是Haskell类约束的线性对应物。线性类型参数允许程序员将文件句柄和手动管理内存等资源作为线性参数进行控制。事实上，线性类型系统可以验证这些资源是否被安全使用。然而，使用显式线性参数编写代码需要繁琐的手续。线性约束解决了这一缺陷：线性约束充当隐式线性参数，可由编译器自动填充。我们将此新功能呈现为一种限定类型系统，并附带一种推理算法，该算法扩展了GHC现有的约束求解器算法。线性约束的正确性通过它们被去糖化为Linear Haskell来确保。本文是同一作者先前论文(arXiv:2103.06127)的修订和扩展版本。形式系统和约束求解器已显著简化，并描述了大量额外应用。