arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2103.06127cs.PL
收藏

线性限定类型:能力和唯一性的泛型推断

Linearly Qualified Types: Generic inference for capabilities and uniqueness

Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard Eisenberg

摘要:

线性参数必须在其函数体中只使用一次。当将文件句柄和手动管理的内存等资源声明为线性参数时,线性类型系统可以验证这些资源是否安全使用。然而,编写带有显式线性参数的代码需要官僚主义。本文介绍了线性约束,这是线性类型的前端特性,可以减少使用线性类型的官僚主义。线性约束是由编译器自动填充的隐式线性参数。我们提出线性约束作为一个合格的类型系统,连同推理算法,扩展GHC的现有约束求解算法。线性约束的合理性是通过将其转换为线性Haskell来保证的。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑