paperbot · PL 论文追踪

RSS

Linearly qualified types: generic inference for capabilities and uniqueness

ICFP 6(ICFP)2022
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

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.

链接与引用

DOI 原文 ·

BibTeX
@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}
}