通过分数唯一性实现函数式所有权
Functional Ownership through Fractional Uniqueness
AI总结：
本文通过将分数权限与分级类型系统相结合，证明 Rust 的所有权模型是唯一性的分级推广，并将其平滑整合到标准类型系统中，扩展了 Granule 语言。
摘要：
所有权与借用系统旨在无需垃圾回收即可强制执行安全的内存管理，Rust 编程语言使这类系统受到广泛关注。Rust 还致力于将函数式编程所提供的一些保证引入高性能系统代码领域，但其类型系统在很大程度上与所有权模型相互分离，类型检查与借用检查在不同的编译阶段进行。RustBelt 和 Oxide 等近期模型旨在对 Rust 进行深入形式化，但较少关注如何将这些基本思想整合到更传统的类型系统中。一种旨在揭示所有权与借用本质核心的方法将为函数式语言借用 Rust 及其他所有权框架中的概念打开大门，从而使更多程序员能够享受其带来的好处。在函数式环境中管理内存的一种策略是唯一性类型，但这些类型提供的视角较为粗粒度：要么一个值恰好只有一个引用，因而可以安全地进行修改；要么由于可能存在其他引用而无法修改。近期工作表明，线性类型和唯一性类型可以在单一系统中结合，从而对程序行为提供限制并对内存使用提供保证。我们进一步发展了这一联系，证明正如 Granule 和 Idris 等分级类型系统推广了线性性一样，Rust 的所有权模型是作为唯一性的分级推广而产生的。我们将分数权限与分级相结合，首次给出了所有权与借用的描述，使其能够与线性类型和分级类型一起平滑地整合到标准类型系统中，并据此用这些思想扩展了 Granule。
英文摘要：
Ownership and borrowing systems, designed to enforce safe memory management without the need for garbage collection, have been brought to the fore by the Rust programming language. Rust also aims to bring some guarantees offered by functional programming into the realm of performant systems code, but the type system is largely separate from the ownership model, with type and borrow checking happening in separate compilation phases. Recent models such as RustBelt and Oxide aim to formalise Rust in depth, but there is less focus on integrating the basic ideas into more traditional type systems. An approach designed to expose an essential core for ownership and borrowing would open the door for functional languages to borrow concepts found in Rust and other ownership frameworks, so that more programmers can enjoy their benefits. One strategy for managing memory in a functional setting is through uniqueness types, but these offer a coarse-grained view: either a value has exactly one reference, and can be mutated safely, or it cannot, since other references may exist. Recent work demonstrates that linear and uniqueness types can be combined in a single system to offer restrictions on program behaviour and guarantees about memory usage. We develop this connection further, showing that just as graded type systems like those of Granule and Idris generalise linearity, Rust's ownership model arises as a graded generalisation of uniqueness. We combine fractional permissions with grading to give the first account of ownership and borrowing that smoothly integrates into a standard type system alongside linearity and graded types, and extend Granule accordingly with these ideas.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
