paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)

函数式、命令式与数独:让好的、坏的和丑的和谐共处(函数式珍珠)
ICFP 8(ICFP)2024匹配度 1/10 · 这篇论文属于函数式编程与 Esterel 并发语言的设计与编程风格讨论,关注的是如何用可变状态和多线程写出易理解的数独求解器,与用户核心方向(静态分析、LLM/Agent 与 PL 交叉、浮点程序分析、贝叶斯程序分析)几乎没有交集。虽然它属于 PL 领域,但不涉及 AI、静态分析、形式化验证或相关 benchmark,因此匹配度很低。引用 1 inbox
Manuel Serrano, Robert Bruce Findler
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:结合函数式编程与 Esterel 式命令式并发,展示用可变状态和多线程也能写出如纯函数式般易理解的数独求解器。

传统观点认为,只要加入少量命令式代码,函数式编程的优势就会消失。本文指出,函数式编程与特殊命令式语言 Esterel 结合能产生倍增收益。二者共享关键限制:函数输出仅由输入决定;Esterel 计算状态仅由程序和上一时间步状态决定,即便程序包含并发线程、可变状态以及线程创建、挂起和中止。作者以 JavaScript 与 Esterel 的混合语言 HipHop 实现数独求解器,深入展示即使使用多线程、可变状态、抢占和线程中止,代码仍可像纯函数式风格一样易于理解;并发组合与任务取消还带来显著的程序结构化收益,支持清晰的分解与任务分离。

问题
论文探讨命令式代码,尤其是并发与可变状态,是否必然破坏函数式编程的可理解性优势,以及如何融合两者以兼得表达力与易推理。
方法
以 Esterel 的时间步语义与函数式输入输出确定性为共同基础,用 JavaScript 与 Esterel 混合语言 HipHop 编写并分析一个数独求解器案例。
评估
通过深入案例研究与程序走查,展示含多线程、可变状态、抢占和线程中止的求解器仍保持纯函数式风格的可理解性,并说明并发组合与任务取消带来的结构分解优势。
原文摘要(Abstract)

Conventional wisdom suggests that the benefits of functional programming no longer apply in the presence of even a small amount of imperative code, as if the addition of imperative code effectively subtracts. And yet, as we show in this paper, combining functional programming with the special imperative language Esterel provides a multiplicative improvement to the benefits of functional programming. The key to the benefit of both Esterel and functional programming stems from a restriction that both share. As in functional programming, where only the inputs to a function determine its outputs, the state of an Esterel computation is fully determined by the program’s input and the state that the computation had in the previous time step, where the notion of a time step is explicit in the language. Esterel’s guarantee holds even though Esterel programs feature concurrent threads, mutable state, and the ability to create, suspend, and even terminate threads as the computation proceeds. This similarity is the root of the benefits that programmers accrue as they informally reason about their program’s behavior. To illustrate these benefits, the bulk of this paper consists of an in-depth exploration of HipHop code (a mashup of JavaScript and Esterel) that implements a Sudoku solver, showing how it is possible to write code that is as easy to understand as if it were written in a pure functional programming style, even though it uses multiple threads, mutable state, thread preemption, and even thread abortion. Even better, concurrent composition and task canceling provide significant program structuring benefits that allow a clean decomposition and task separation in the solver.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{SerranoF24,
  title = {The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)},
  author = {Manuel Serrano and Robert Bruce Findler},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {ICFP},
  year = {2024},
  doi = {10.1145/3674631}
}