Verse Calculus:失败为什么不是布尔值

一、一篇论文,回答一个怪问题

2023 年,Epic 的语言团队在函数式编程顶级会议 ICFP 上发表了论文《The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming》。作者名单相当豪华:Lennart Augustsson、Joachim Breitner、Koen Claessen、Ranjit Jhala、Simon Peyton Jones(Haskell 的灵魂人物之一)、Olin Shivers,以及 Epic 创始人 Tim Sweeney 本人。论文干的事,是把 Verse 蒸馏成一个极小的「核心演算」——就像 λ 演算之于函数式语言——并给出小步重写语义,让你可以像做代数一样推理 Verse 程序。

2023 年,Epic 的语言团队在函数式编程的顶级会议 ICFP 上发表了论文《The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming》。作者名单相当豪华:Lennart Augustsson、Joachim Breitner、Koen Claessen、Ranjit Jhala、Simon Peyton Jones(Haskell 语言的灵魂人物之一)、Olin Shivers,以及 Epic 创始人 Tim Sweeney 本人。论文干的事,是把 Verse 提炼成一套极小的「核心规则」——小到可以像中学做代数题那样,一步一步推演一段 Verse 程序会怎么跑,从而把整门语言的行为讲得严丝合缝。

论文的标题已经把 Verse 的血统说白了:它是一门确定性函数式逻辑语言。「函数式」这半边它继承自 Haskell 一系:一切皆表达式,绑定默认单赋值;「逻辑」那半边则和 Prolog 沾亲:程序可以「找不到答案」,而这件事本身就是受控的控制流。

论文标题已经把 Verse 的血统说白了:它是一门确定性的「函数式 + 逻辑」语言。「函数式」这半边的意思是——程序里几乎每一步都是「算出一个值」,而且变量默认只设一次、之后不再改(它这套基因来自 Haskell 一系语言);「逻辑」那半边的意思是——一段程序允许「找不到答案」,而「找不到答案」这件事本身,就是一种受控的分支走向(这套基因和 Prolog 沾亲)。

二、失败是控制流,不是值

在这个内核里,失败(fail)和选择(choice)是一等语义原语:一个表达式求值,要么产出结果,要么失败——空手而归。条件分支由「表达式有没有结果」驱动,而不是由某个布尔值驱动。这就是第 7 课那句话的理论出处:if 检查的从来不是「true 还是 false」,而是「这次求值成功了吗」。布尔值在内核里甚至不是必需品——logic 只是把这种控制流具体化成一个可以存进变量的值,而 logic{} 恰好就是两个世界之间的那座官方桥梁:

在这套核心规则里,「失败」和「二选一」是最基本的两个原始动作:任何一步求值,要么算出一个结果,要么失败——空手而归。分支走哪条,由「这一步有没有算出结果」决定,而不是由某个 true/false 决定。这正是第 7 课那句话的理论出处:if 检查的从来不是「打勾还是没打勾」,而是「这一步走通了吗」。true/false 在这套规则里甚至不是必需品——logic 只是把「走没走通」这种走向固化成一个能存进变量的开关值,而 logic{} 恰好就是这两个世界之间那座官方桥梁:

using { /UnrealEngine.com/Temporary/Diagnostics }

# 这两行问的是完全不同的问题:

# 「Score > 100 这次求值,有结果吗?」——成败世界
if (Score > 100):
    Print("达标!")

# 「把这次成败封存成一枚可存放的值」——真假世界
HasWon := logic{Score > 100}

▸ 读图翻译:上下两段问的是两个不同的问题。上面那段等于一个 Branch:「Score > 100 这条线走得通吗?」走通就打印。下面那段没有分叉,而是把「Score > 100 走不走得通」的结果封成一个开关值 HasWon 存起来备用——就是本课那个反向旋转门。

顺着这个视角,第 7 课乃至前几课的许多「怪规矩」会一口气全部解释通。为什么 = 是比较而不是赋值?因为在逻辑语言里,= 表达的是「让两边相等/检查两边相等」,它可能失败,所以它是可失败表达式。为什么没有语句、只有表达式?函数式血统使然。为什么 if 里的 set 在整体失败时会回滚(讲变量时提过的事务性,对应 <transacts> 效果)?因为失败是受控的语义事件,语言有义务把「失败的尝试」擦干净,仿佛什么都没发生过——这正是确定性的代价与承诺。

顺着这个视角,第 7 课乃至前几课的许多「怪规矩」会一口气全部讲通。为什么 = 是「比较」而不是「赋值」?因为在这种语言里,= 问的是「让两边相等 / 两边真的相等吗」,这一问可能失败,所以它也是一次「走不走得通」。为什么每一步几乎都在「算出一个值」、很少见到纯粹的命令句?这是它函数式血统使然。为什么一段 if 整体没走通时,里面已经做过的 set 会被撤销(讲变量时提过的事务性,对应 <transacts> 标记)?你可以想成:引擎先在一张「影子图」上把这段试连一遍,全部走通了才真正落到主图上;中途走不通,就当这段从没连过、痕迹全部抹掉——这正是「确定性」的代价,也是它的承诺。

三、这对每天写代码的你意味着什么

不打算读论文也没关系,带走一个心智模型就值回票价:在 Verse 里,凡是出现条件的地方,问的都是「有没有结果」,不是「是不是 true」。用这个模型去看 if (MyLogic?) 的问号、去看数组下标 Items[0] 为什么要待在 if 里、去看下一课的失败上下文,一切都是同一件事的不同侧脸。语言不是在为难你,它只是从头到尾只讲一种逻辑。

不打算读论文也没关系,带走一个心智模型就值回票价:在 Verse 里,凡是出现条件判断的地方,问的都是「这一步有没有结果」,不是「是不是打了勾」。用这个模型去看 if (MyLogic?) 的问号、去看「从数组里按序号取一个元素」(Items[0])为什么非要待在 if 里(因为序号可能越界、取不到——那也是一次「走不通」)、去看下一课的失败上下文,会发现全是同一件事的不同侧脸。语言不是在为难你,它只是从头到尾只讲一种逻辑。

想深挖的读者,论文 PDF 公开可读(见文末来源),前几节的重写规则配着例子并不难跟前几节那套推演规则配着例子并不难跟;读完你大概率会对「Verse 与 Haskell、Prolog 的亲缘关系」这句话产生具体的体感。这也是判断一门新语言值不值得深学的小窍门:看它背后有没有一个能自圆其说的内核。Verse 有,而且发表在了顶会上。

来源

本文整理自公开论文与会议资料:The Verse Calculus — Simon Peyton Jones 个人主页(含 PDF)↗ · ACM Digital Library 收录页 ↗ · ICFP 2023 会议页 ↗