Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
复制标题
多态可达性类型：跟踪高阶通用程序中的新鲜度、别名和分离
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Tiark Rompf
中科院分区：
文献类型：
--
作者：
Guannan Wei;Oliver Bračevac;Songlin Jia;Yuyan Bao;Tiark Rompf
在Rust成功的推动下，许多编程语言都在其类型系统中添加子结构特性。跟踪生命周期和共享等属性的承诺是巨大的，不仅用于低级内存管理，还用于控制高级资源和功能。但是，将成功的技术从Rust应用到更高级的语言中也存在困难，因为这些技术需要与其他高级特性进行交互，尤其是各种风格的函数和类型级抽象。怎样才能把关于生命周期和共享的完整的推理带到主流语言中呢？可达性类型是最近的一个提议，它在扩展到高阶但单态的设置方面显示出了希望，在分离逻辑的启发下，在基板上跟踪混叠和分离。然而，在具有类型多态性和/或精确可达性多态性的先验可达性类型系统λ*之上的幼稚扩展是不健全的，使得λ*不适合在实际语言中采用。结合可达性和精确、可靠和参数化的类型多态性仍然是一个开放的挑战。本文对可达性跟踪设计进行了反思，提出了一种新的多态可达性类型系统。我们引入了一个新的新鲜度限定符来指示其可达性集可能在评估步骤中增长的变量。新系统跟踪单步可达的变量，并仅在必要时计算传递闭包，从而保留可达的已知变量链，这些已知变量可以使用替代进行细化。这些思想产生了具有精确轻量级（即无量词、可达性多态性）的简单类型λ -演算，以及具有类型和可达性限定符上有界参数多态性的F<: -演算，为真正跟踪生命周期和主流语言的共享实践铺平了道路。证明了Coq的类型稳健性和分离性的保存性。我们讨论了各种应用程序（例如，安全能力编程），可能的效果系统扩展，并将我们的系统与Scala的捕获类型进行了比较。
Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting successful techniques from Rust to higher-level languages, where they need to interact with other advanced features, especially various flavors of functional and type-level abstraction. What would it take to bring full-fidelity reasoning about lifetimes and sharing to mainstream languages? Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. However, naive extensions on top of the prior reachability type system λ* with type polymorphism and/or precise reachability polymorphism are unsound, making λ* unsuitable for adoption in real languages. Combining reachability and type polymorphism that is precise, sound, and parametric remains an open challenge. This paper presents a rethinking of the design of reachability tracking and proposes new polymorphic reachability type systems. We introduce a new freshness qualifier to indicate variables whose reachability sets may grow during evaluation steps. The new system tracks variables reachable in a single step and computes transitive closures only when necessary, thus preserving chains of reachability over known variables that can be refined using substitution. These ideas yield the simply-typed λ✦-calculus with precise lightweight, i.e., quantifier-free, reachability polymorphism, and the F<:✦-calculus with bounded parametric polymorphism over types and reachability qualifiers, paving the way for making true tracking of lifetimes and sharing practical for mainstream languages. We prove type soundness and the preservation of separation property in Coq. We discuss various applications (e.g., safe capability programming), possible effect system extensions, and compare our system with Scala’s capture types.
登录
查看更多内容
可达性类型：跟踪高阶函数程序中的别名和分离
影响因子：
--
作者：
Bao, Yuyan;Wei, Guannan;Bračevac, Oliver;Jiang, Yuxuan;He, Qiyang;Rompf, Tiark
通讯作者：
Rompf, Tiark
非纯高阶语言的图 IR：通过精确的效果依赖性使积极的优化变得经济实惠
影响因子：
--
作者：
Bračevac, Oliver;Wei, Guannan;Jia, Songlin;Abeysinghe, Supun;Jiang, Yuxuan;Bao, Yuyan;Rompf, Tiark
通讯作者：
Rompf, Tiark
通用 Java 的通用所有权
影响因子：
--
作者：
Potanin A
通讯作者：
Potanin A
多态可迭代序列效应系统
影响因子：
1.3
作者：
Gordon, Colin S.
通讯作者：
Gordon, Colin S.