Verse 的理论根基:确定性函数逻辑编程
「if 测的是成败,不是真假」并非拍脑袋的语法怪癖——它出自一篇正经的学术论文。这一页带你远眺 Verse 的理论底座 The Verse Calculus:失败与选择如何成为语言的一等公民,以及这对每天写设备代码的你意味着什么。
一、这门语言有论文护体
大多数游戏脚本语言的诞生方式是「先能跑,再补文档」。Verse 反着来:它是一门确定性函数逻辑语言(deterministic functional logic language),其核心演算 The Verse Calculus 以论文形式发表在编程语言领域的顶级会议 ICFP 2023 上。作者阵容相当豪华:Lennart Augustsson(Haskell 最早的编译器作者之一)、Simon Peyton Jones(Haskell 之父之一、GHC 的灵魂人物)、Tim Sweeney(Epic Games 创始人)等人联手。让写出 Haskell 的人来设计一门游戏脚本语言——这大概是「用料过猛」在语言设计界的样子。
「函数逻辑语言」这个门派,结合了函数式编程(表达式、不可变值、组合)与逻辑编程(把「找到满足条件的解」交给语言本身)。而「确定性」是 Verse 的自我约束:同样的输入永远给出同样的结果,不会像某些逻辑语言那样给出「随缘」的解。第 8 课里所有看起来特立独行的设计——if 测成败、失败可回滚、没有异常机制——在这篇论文里都有严格的数学定义。
「函数逻辑语言」这个门派,把两种风格揉在了一起:一种是函数式——万物都是「算出一个值」,算完不到处乱改数据;另一种是逻辑式——你只描述「什么样的解才算数」,真正去找解的活儿交给语言本身。而「确定性」是 Verse 给自己立的规矩:同样的输入永远给同样的结果,不会像某些逻辑语言那样丢给你一个「随缘」的答案。第 8 课里那些看着特立独行的设计——if 测成败、失败能回滚、没有报错崩溃这一套——在这篇论文里全都有严格的数学定义。
二、零个值、一个值、许多值
论文的核心洞察可以用一句话讲完:把「失败」和「选择」当作语言的一等公民。在传统语言里,一个表达式恰好产生一个值,天经地义;在 Verse 的语义模型里,一个表达式可以产生零个、一个或多个值:
论文的核心洞察一句话就能讲完:把「失败」和「选择」当成语言的头等大事。在传统写法里,你算一样东西,天经地义地就得到一个值;而在 Verse 的模型里,算一样东西可以给出零个、一个、甚至好几个值:
# 语义示意(不能这样裸写:可失败表达式必须待在失败上下文里)
# 一个值:比较成立,表达式成功
3 < 5
# 零个值:比较不成立,表达式「失败」——不是 false,是没有值
5 < 3
# if 的真面目:条件产出至少一个值就走 then,零个值就走 else
if (X := Items[0]):
Print("拿到 {X}")
else:
Print("这次产出了零个值")「失败」在这套语义里的精确定义就是:表达式产生了零个值。所以 Verse 的 if 从来不需要布尔值——它只需要数一数条件产出了几个值:至少一个,走 then(还顺手把值绑定给你);零个,走 else。「多个值」则对应「选择」:一个表达式可以给出多个候选值,for 的生成器语义正是建立在这上面——这也是为什么第 10 课你会看到 for 能把每次迭代的结果收集成数组。if 与 for 不是两套机制,而是同一套「值的产出与收集」语义的两张面孔。
「失败」在这套说法里的精确定义就是:这次运算产生了零个值。所以 Verse 的 if 压根不需要什么布尔值——它只是数一数条件产出了几个值:至少一个,走 then(顺手把那个值存给你用);一个都没有,走 else。「多个值」则对应「选择」:一次运算可以摆出好几个候选值,for / ForEach 之所以能逐个取值,正是建立在这上面——这也是为什么第 10 课你会看到 for 能把每轮的结果收集成一个数组。if 和 for 不是两套东西,而是同一套「值怎么产出、怎么收集」的两张面孔。
论文还为这套语义给出了小步重写规则(small-step rewrite semantics):Verse 程序可以像 lambda 演算一样,通过一步步等价改写来推理——「这两段程序等价吗」从玄学变成可以证明的命题。这为编译器优化(包括第 8 课拓展页提到的宽松求值)提供了安全网:只要改写规则证明等价,编译器就敢大胆重排你的代码。
论文还给这套语义配了一套「一步步等价改写」的推理规则(叫 small-step rewrite semantics):两段程序到底等不等价,从「凭感觉」变成了能严格证明的事。这就给引擎优化(包括第 8 课拓展页说的宽松求值)上了一道保险:只要证明改写前后等价,引擎就敢放心大胆地重排你的逻辑。
三、这对写设备代码的你意味着什么
你不需要读懂论文里的希腊字母也能写好 Verse,但知道底座的存在,有三个实际的好处。其一,语义是统一的:if 的条件、for 的过滤、? 解包 option、方括号调用可失败函数——它们全是「产出零个或一些值」这一件事的不同外衣,学会一个等于学会全部。其二,回滚是可信的:推测执行与效果回滚在演算层面有严格定义,不是运行时打的补丁,所以你可以放心把「试探性修改」写进失败上下文。其三,限制是有理由的:禁止 return、禁止条件里的副作用,都是为了保住「程序可等式推理」这块基石——编译器拦你,不是刁难,而是替这套数学模型站岗。
你不用读懂论文里那些希腊字母也能写好 Verse,但知道底座在那儿,有三个实打实的好处。其一,讲法是统一的:if 的条件、for / ForEach 的过滤、用 ? 取出 option、用方括号调用可失败函数——它们全是「产出零个或若干个值」这同一件事的不同外衣,学会一个等于学会一片。其二,回滚是可信的:推测执行(那张「影子图」)和效果回滚在演算层面有严格定义,不是事后打的补丁,所以你可以放心把「试探性的改动」写进失败上下文。其三,限制是有道理的:禁止 return、禁止在条件里做会改动世界的动作,都是为了守住「两段程序能不能用等号推来推去」这块基石——编译器拦你,不是刁难,是替这套数学模型站岗。
换句话说:当你在 UE6 里写下一句 if (Player := player[Agent]):,背后站着的是三十年函数式编程研究的家底。这在游戏脚本语言里,是相当奢侈的待遇。
按照 Verse Calculus 的语义模型,「失败」最准确的描述是哪一个?
四、来源与延伸
本文依据论文作者公开发布的资料整理。想亲自翻一翻原文(英文,预警:有希腊字母),这几个入口按友好程度排序:
▸ The Verse Calculus 项目页(Simon Peyton Jones 主页)↗
▸ 论文 PDF:The Verse Calculus — a core calculus for deterministic functional logic programming ↗
读不动全文完全不影响通关本教程——但下次有人问你「为什么 Verse 的 if 这么怪」,你可以云淡风轻地回一句:「那不是怪,那是确定性函数逻辑编程。」