一句话:提出线性完全原地(FIP)演算,证明一类纯函数式程序可无分配、常量栈空间地原地执行,并在 Koka 中实现。
函数式程序员常面临两难:是写纯函数代码,还是为效率牺牲纯度而使用原地更新?本文精确刻画了何时能兼得二者:一大类纯函数式程序在其参数不被共享时,可安全地用原地更新执行而无需内存分配。作者提出线性“完全原地”(FIP)演算,并证明此类函数总能无(去)分配地执行且使用常量栈空间。他们给出伸展树、手指树等数据结构上的原地函数,以及原地归并排序和快速排序,并证明可对任意多项式数据类型泛型推导出完全原地的 map 函数。最后在 Koka 语言中实现 FIP 演算规则,借助 Perceus 引用计数垃圾回收,在可能时动态地原地执行 FIP 函数。
As functional programmers we always face a dilemma: should we write purely functional code, or sacrifice purity for efficiency and resort to in-place updates? This paper identifies precisely when we can have the best of both worlds: a wide class of purely functional programs can be executed safely using in-place updates without requiring allocation, provided their arguments are not shared elsewhere. We describe a linear _fully in-place_ (FIP) calculus where we prove that we can always execute such functions in a way that requires no (de)allocation and uses constant stack space. Of course, such a calculus is only relevant if we can express interesting algorithms; we provide numerous examples of in-place functions on datastructures such as splay trees or finger trees, together with in-place versions of merge sort and quick sort. We also show how we can generically derive a map function over _any_ polynomial data type that is fully in-place. Finally, we have implemented the rules of the FIP calculus in the Koka language. Using the Perceus reference counting garbage collection, this implementation dynamically executes FIP functions in-place whenever possible.
@article{paperbot1911,
title = {FP²: Fully in-Place Functional Programming},
author = {Anton Lorenzen and Daan Leijen and Wouter Swierstra},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607840}
}