Verse 演算:给函数式逻辑编程一个数学核心

一、一门游戏语言,一篇 ICFP 论文

2023 年,Simon Peyton Jones、Tim Sweeney、Lennart Augustsson 等八位作者在函数式编程领域的顶级会议 ICFP 上发表了论文《The Verse Calculus: a core calculus for deterministic functional logic programming》。工业界为自家脚本语言写形式化论文本就少见,更少见的是这份作者名单——语言的老板(Sweeney)和函数式编程的宗师(Peyton Jones)并排署名。

这篇论文做的事,可以用一个类比讲清楚:lambda 演算之于函数式语言,就是 Verse 演算之于 Verse。lambda 演算是一套极简的数学规则,所有函数式语言的行为最终都能还原到它身上;Verse 演算则是 Verse 的这套「最小内核」——把语法糖全部剥掉之后,剩下的那台不会骗人的裸机。Verse 演算就是 Verse 剥到只剩骨架后的「最小内核」。数学家惯用的招数,是给一门语言配一套极简、不会骗人的规则,让语言里发生的一切最终都能还原到这套规则上;把那些只是让代码写起来顺手的便捷写法全部剥掉之后,剩下的就是这台裸机。

二、内核三件套:合一、选择、确定性

Verse 演算的核心思想有三条,每一条都对应你在正课里会遇到的「怪设计」:

• ◇ 变量靠合一(unification)绑定。变量不是「一个装值的盒子」,而是「一个待解的未知数」;程序运行的过程,有点像解方程——让等式两边成立。这就是为什么 Verse 里单独的 = 是「可失败的相等」而不是赋值而不是把值塞进变量(塞值那件事,在蓝图里是 Set 节点,在 Verse 里写作 set)。
• △ 表达式可以产出多个值(choice 选择序列)。一个表达式的结果不一定是一个值,可能是一串候选值组成的「选择空间」。for 干的事,本质上就是把一个表达式的所有成功值遍历一遍。
• △ 一段计算可以吐出好几个值(叫「选择序列」)。一段计算的结果不一定只有一个值,可能是一串候选值组成的「选择空间」。而 for(就是蓝图里的 ForEach Loop)干的事,本质上就是把这一串成功的值挨个走一遍。
• ▢ 整门语言是「确定性的」函数式逻辑编程。逻辑式语言常被诟病结果依赖求解顺序,而 Verse 演算保证:同一个程序,总有唯一的结果。你写的关卡逻辑不会「今天跑出这个结果、明天跑出那个」。
• ▢ 整门语言是「确定性的」——同一个程序,永远只跑出同一种结果。有些编程流派会因为内部求值顺序不同而给出不同答案,而 Verse 从数学上堵死了这种可能:你写的关卡逻辑不会「今天跑出这个结果、明天跑出那个」。

论文为这套内核给出了小步重写语义(small-step rewrite semantics)——程序如何一小步一小步地被改写、化简,并证明了对行为良好的项,这个重写系统是合流的(confluent):不管你按什么顺序化简,最终都汇到同一个结果。这意味着你可以像推导数学公式一样,对 Verse 程序做等价变换——编译器优化、程序验证,都因此有了坚实的地基。

三、把理论映射回你写的代码

听起来很玄?其实你在正课第 1 课就已经踩在这套理论上了。看两个最小示例:

# = 不是赋值,是一次「可失败的相等」
# 可失败表达式只能住在 if 这样的失败上下文里
if (2 + 2 = 4):
    Print("数学没有崩坏")

# for 遍历的是一段表达式的整个「成功空间」
for (I := 1..3):
    Print("回合 {I}")

读图翻译(蓝图视角):上半段就是一个 Branch 节点——只不过它问的不是 True/False,而是「2 + 2 = 4 这条线走不走得通」,走通了才接着打印。下半段是一个 ForEach Loop:1..3 相当于一个装着 1、2、3 的数组,循环体里那句 Print 会被逐个跑三遍,于是日志里出现三行「回合」。

第一段:2 + 2 = 4 是一次相等测试,成立则 if 的分支执行,不成立就安静地失败——没有 true/false 在代码里流动,「失败」本身取代了布尔值。第二段:1..3 在演算的视角下是一个产出 1、2、3 三个值的选择序列,for 把这个选择空间走了一遍,于是日志里出现三行「回合」。教程里的「掷骰子」「失败上下文」这些比喻,论文里都有一个精确的数学对应物。

如果想听作者亲口讲这套设计,Peyton Jones 与 Sweeney 在 Lambda Days 2023 的联合演讲《Beyond functional programming: a taste of Verse》是最好的入门材料——一小时里把「if 即失败上下文」「for 即遍历选择空间」讲得明明白白。

四、小测一下

来源与延伸

本文整理自 Simon Peyton Jones 个人主页的论文专页与 Lambda Days 2023 公开演讲:

• The Verse Calculus 论文页(simon.peytonjones.org)↗
• 演讲《Beyond functional programming: a taste of Verse》(YouTube)↗