一句话：为纯函数式语言的 do 记法加入局部可变、提前返回与迭代，并给出到纯函数代码的翻译及 Lean 正确性证明。
纯函数式语言通过 monad 等抽象将隐式效果显式化，但常见 do 记法在简洁性上仍不如其模仿的命令式代码。本文作为 functional pearl，探索在 do 记法中引入局部可变、提前返回和迭代等命令式特性，以简化 monadic 代码。作者给出一组形式化翻译规则，将这些特性编译回纯函数式代码，并在 Lean 4 定理证明器中实现该翻译；基于简单的静态与动态语义，形式证明翻译规则的正确性，说明生成的代码仍可推理。该工作提供了兼具命令式书写便利与纯函数式语义保证的语言机制。
Purely functional programming languages pride themselves with reifying effects that are implicit in imperative languages into reusable and composable abstractions such as monads. This reification allows for more exact control over effects as well as the introduction of new or derived effects. However, despite libraries of more and more powerful abstractions over effectful operations being developed, syntactically the common 'do' notation still lags behind equivalent imperative code it is supposed to mimic regarding verbosity and code duplication. In this paper, we explore extending 'do' notation with other imperative language features that can be added to simplify monadic code: local mutation, early return, and iteration. We present formal translation rules that compile these features back down to purely functional code, show that the generated code can still be reasoned over using an implementation of the translation in the Lean 4 theorem prover, and formally prove the correctness of the translation rules relative to a simple static and dynamic semantics in Lean.
@article{paperbot1497,
title = {‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)},
author = {Sebastian Ullrich and Leonardo de Moura},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547640}
}