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风格的非局部借用仍属未知——在Rust风格中，每个借用者可以自由拆分和丢弃，而无需向借出者直接通信所有权。我们通过Pure Borrow——一个在Linear Haskell中实现纯Rust式借用的新颖框架——对此问题给出了肯定回答。值得注意的是，与IO单子、ST单子及现有Linear Haskell API不同，它支持纯计算中带有仿射可变引用的并行状态可变性。相较于Rust，它还享有纯度、惰性求值、一等多态性和无泄漏性。我们仅将Pure Borrow作为Linear Haskell的一个库实现，并通过一个并行计算案例研究展示了其能力。我们形式化了Pure Borrow的核心，并构建了一个元理论，该理论借助一种新的、基于历史的借用模型，致力于建立安全性、无泄漏性和合流性。