为什么 Verse 默认不可变:函数式逻辑语言的设计哲学

一、三个「怪癖」,其实是同一件事

学完第 4 课,你手里攒了三个疑问。为什么「不可变」是默认,「可变」反而要申请 var?为什么修改必须喊 set,连个偷懒的写法都不给?为什么 = 是比较而且 Verse 干脆没有 ==?在 C 系语言的世界观里,这三条都是反常识的。但它们其实是同一个设计决定在三个位置的投影。

学完第 4 课,你手里攒了三个疑问。为什么「不可变」是默认,「可变」反而要专门加 var?为什么改值必须接 Set,连个偷懒的写法都不给?为什么 = 是比较、而且 Verse 干脆没有 ==?在大多数常见语言的习惯里,这三条都反常识。但它们其实是同一个设计决定在三个位置的投影。

这个设计决定写在一篇正式发表的论文里:The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming(ICFP 2023),作者阵容相当豪华——Lennart Augustsson、Joachim Breitner、Koen Claessen、Ranjit Jhala、Simon Peyton Jones(Haskell 之父之一)、Olin Shivers,以及 Epic 的 Tim Sweeney 本人。论文给 Verse 建立了一个数学内核:确定性函数式逻辑演算。翻译成人话:Verse 的骨子里更接近 Haskell 和 Prolog 的混血,而不是 C++ 的近亲。翻译成人话:Verse 骨子里更像「数学证明 + 逻辑推理」那一类语言,而不是你常见的那种「一句句下命令」的语言。

二、一切皆表达式,绑定默认单赋值

在这个演算里,没有「语句」这种东西——一切都是表达式,都有值(或者失败)。if 是表达式,代码块是表达式,连你以为是「赋值语句」的东西也是表达式。而名字和值的关系,默认是绑定(binding)而非存储(storage):X := 5 的本意是「让 X 与 5 绑定」,一次绑定,终身有效——这就是第 4 课里「常量是默认」的来历。

在这个演算里,没有「语句」这种东西——一切都是「表达式」,每样东西都会算出一个值(或者失败)。if 会算出值,一整块代码会算出值,连你以为是「赋值命令」的东西也会算出值。而名字和值的关系,默认是绑定(binding)而不是存储(storage):X := 5 的本意是「让 X 和 5 绑在一起」,绑一次,终身有效——这就是第 4 课里「常量是默认」的来历。

于是 = 的身份也顺理成章了:在逻辑语言的传统里,X = 5 读作「断言 X 与 5 相等」。断言成立,表达式成功;不成立,表达式失败——而失败不是异常、不是崩溃,是 Verse 里一等公民的控制流(你会在条件判断的章节里正式和它打交道)。所以 Verse 不需要 ==:它的 = 从来就是提问,从来不是覆盖。真正的「覆盖」是被单独圈出来的危险操作,必须挂上 var 的申请、喊出 set 的口令——可变状态在这门语言里是明码标价的例外,而不是空气一样的默认。

于是 = 的身份也顺理成章了:在逻辑推理这类语言的传统里,X = 5 读作「断言 X 和 5 相等」。断言成立,这一步就走通;不成立,就走不通——而「走不通」不是报错、不是崩溃,它是 Verse 里正儿八经的一条控制流分支(你会在讲 Branch 那种判断的章节里正式和它打交道)。所以 Verse 不需要 ==:它的 = 从来就是提问,从来不是覆盖。真正的「覆盖」是被单独圈出来的危险操作,必须先加上 var、再接一个 Set——可变状态在这门语言里是明码标价的例外,而不是像空气一样的默认。

三、失败就回滚:被「事务」保护的 set

这套世界观最惊艳的推论是:赋值是可以撤销的。当 set 发生在一个可失败的表达式内部(比如 if 的条件区),而这个表达式最终失败时,Verse 会把这次修改整个回滚——就像数据库事务一样,要么全成,要么像没发生过。这个能力与函数的 <transacts> 效果标注绑定。看个例子:

这套世界观最惊艳的推论是:改值是可以撤销的。当一个 Set 发生在「可能走不通的判断」内部(比如 Branch 的条件区),而这个判断最终走不通时,Verse 会把这次修改整个回滚——就像数据库事务一样,要么全成,要么像没发生过。这个能力和函数的 <transacts> 效果标注绑定。看个例子:

using { /Fortnite.com/Devices }
using { /UnrealEngine.com/Temporary/Diagnostics }

rollback_demo_device := class(creative_device):

    var Gold:int = 100

    OnBegin<override>()<suspends>:void =
        if:
            set Gold = 999
            Gold > 1000
        then:
            Print("押注成功")
        Print("Gold: {Gold}")

条件区里先 set Gold = 999,再检查 Gold > 1000——999 不大于 1000,条件整体失败。于是那次 set 被回滚,最后一行打印的是 Gold: 100,仿佛什么都没发生。在 C++ 或 JS 里,想要「试着改一下,不行就恢复原样」,你得自己备份旧值、自己写恢复逻辑、自己保证每条失败路径都恢复到位;在 Verse 里,这是语言内建的语义。

读图翻译:条件区里先接一个 Set 把 Gold 改成 999,再检查 Gold > 1000——999 不大于 1000,这个判断整体走不通。于是刚才那次 Set 被回滚,最后一行 Print String 打出来的是 Gold: 100,仿佛什么都没发生。换别的语言,想要「试着改一下,不行就恢复原样」,你得自己先备份旧值、自己写恢复逻辑、自己保证每条失败岔路都恢复到位;在 Verse 里,这是语言内建就管好的行为。

现在回望第 4 课:强制 set 不只是防手滑——正因为每一次修改都被显式标记,编译器才能精确追踪「哪些修改发生在可失败的范围里」,回滚才可能自动化;而「默认不可变」让绝大多数代码根本无状态可回滚,推理起来像数学一样干净。论文为这套语义给出了小步重写规则,你可以像推导 λ 演算一样在纸上推导一段 Verse 程序的行为。想深挖的话,论文 PDF 公开可读——对一门游戏脚本语言来说,这样的理论底座相当奢侈。

现在回望第 4 课:强制接 Set 不只是防手滑——正因为每一次修改都被明确标出来,编译器才能精确追踪「哪些修改发生在可能走不通的范围里」,回滚才可能自动化;而「默认不可变」让绝大多数代码根本没有状态需要回滚,推理起来像数学一样干净。论文为这套规则给出了一步步的重写推导,你可以像在纸上推演公式一样,推演一段 Verse 程序的行为。想深挖的话,论文 PDF 公开可读——对一门游戏脚本语言来说,这样的理论底座相当奢侈。

四、小测验

来源

本文整理自 Verse Calculus 论文及其公开资料:The Verse Calculus 项目页(Simon Peyton Jones)↗ · 论文 PDF(ICFP 2023)↗ · ACM Digital Library 收录页 ↗