A promising approach to unifying functional and imperative programming paradigms is to localize mutation using linear or affine types. Haskell, a purely functional language, was recently extended with linear types by Bernardy et al., in the name of Linear Haskell. However, it remained unknown whether such a pure language could safely support non-local borrowing in the style of Rust, where each borrower can be freely split and dropped without direct communication of ownership back to the lender. We answer this question affirmatively with Pure Borrow, a novel framework that realizes Rust-style borrowing in Linear Haskell with purity. Notably, it features parallel state mutation with affine mutable references inside pure computation, unlike the IO and ST monads and existing Linear Haskell APIs. It also enjoys purity, lazy evaluation, first-class polymorphism and leak freedom, unlike Rust. We implement Pure Borrow simply as a library in Linear Haskell and demonstrate its power with a case study in parallel computing. We formalize the core of Pure Borrow and build a metatheory that works toward establishing safety, leak freedom and confluence, with a new, history-based model of borrowing.

翻译：一种有前景的统一函数式与命令式编程范式的方法是通过线性或仿射类型局部化可变性。Haskell作为一种纯函数式语言，近期由Bernardy等人以Linear Haskell之名扩展了线性类型。然而，尚不清楚这种纯语言能否安全地支持Rust风格的非局部借用——其中每个借用者可自由拆分与丢弃，无需向出借者直接通讯所有权。我们通过Pure Borrow（一种在Linear Haskell中实现Rust风格借用并保持纯度的新型框架）对此问题给出肯定回答。值得注意的是，该框架在纯计算内部实现了带仿射可变引用的并行状态可变性，不同于IO与ST单子及现有Linear Haskell API。与Rust不同，它兼具纯度、惰性求值、一等多态性与无泄漏特性。我们将Pure Borrow简单实现为Linear Haskell库，并通过并行计算案例研究展示其能力。我们形式化了Pure Borrow的核心机制，并建立元理论以通过基于借用历史的新模型来论证安全性、无泄漏性与合流性。