A linear argument must be consumed exactly once in the body of its function. A linear type system can verify the correct usage of resources such as file handles and manually managed memory. But this verification 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 to be filled in automatically by the compiler. Linear constraints are presented as a qualified type system, together with an inference algorithm which extends OutsideIn, GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.
翻译:线性参数必须在其函数正文中完全消化一次。 线性类型系统可以核查文件把手和手动管理的内存等资源的正确使用。 但这种核查需要官僚主义。 本文提供了线性限制, 这是线性打字的前端特征, 减少了线性工作类型的官僚主义。 线性限制是线性隐含的线性参数, 由编译者自动填充。 线性限制作为合格的类型系统提出, 连同一种推算算算算法, 延伸到GHC现有的限制解算法OuterIn。 线性限制的正确性得到保证, 因为它们会将线性限制从苏加尔运入Linear Haskell。