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., named Linear Haskell. However, it remained unknown whether such a pure language could safely support non-local \emph{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 by \emph{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的核心，并构建了一个元理论，致力于借助一种新颖的基于历史的借用模型来建立安全性、泄漏自由性和合流性。