企业官网建设流程全解析

• 编程语言
• 编译器
• 语言运行时
• 开发工具

导读

fix-annotated-lambdas.md是 Unison 代码仓库中一份用于回归测试的 idempotent transcript，专门覆盖"带类型注解的 lambda 在编译期浮动（floating）过程中被错误改写"这一历史缺陷。阅读本文后，你将掌握：该测试用例的完整结构与运行方式、foo/bar示例背后的 Rank-2 多态与 lambda 浮动原理、Unison 编译器 ANF 变换阶段如何处理Ann'与LamsAnnot形式，以及如何通过display命令验证浮动结果不丢失注解语义。

一、这份文档是什么：一份"幂等"回归测试 transcript

在 Unison 仓库中，unison-src/transcripts/idempotent/目录存放着一批幂等 transcript：它们以 Markdown 为载体，内嵌ucm（Unison Codebase Manager）交互命令与unison代码块，由 transcript 运行器（见 unison-cli/transcripts/Transcripts.hs）逐段执行并回填输出。"幂等"意味着这些测试反复运行时结果保持一致，适合作为持续集成的回归防线。

fix-annotated-lambdas.md 全文围绕一句话展开：

Tests an erroneous lambda floating case involving annotations.

即：验证一个与"带类型注解的 lambda 浮动"相关的错误案例是否已被修复。文档正文只保留了三类内容——初始化命令、复现用例代码、以及期望的 UCM 输出。它不讲解理论，而是把"修复后必须得到的结果"固定成可机器校验的断言。

二、复现用例：Rank-2 多态注解下的 lambda

文档中用于复现缺陷的 Unison 代码块如下：

foo : a -> a foo x = bar ((f -> f x) : forall r. (a -> r) -> r) bar : (forall r. (a -> r) -> r) -> a bar k = k (x -> x)

这段代码包含两个需要留意的关键要素：

1. bar接受一个 Rank-2 多态参数。bar的类型是(forall r. (a -> r) -> r) -> a，即它期望的参数本身带有一个forall r.的全称量化类型，这不同于普通的一阶多态参数。
2. foo内部用一个显式类型注解: forall r. (a -> r) -> r标注了内层 lambda(f -> f x)。该注解声明了这个 lambda 必须是多态的：对任意类型r，它都能把一个a -> r的函数应用于x。

这正是"lambda 浮动"最容易出错的地方。Unison 编译器在生成后端代码前会把嵌套的 lambda 提升（浮动/hoisting）为可共享的顶层或命名绑定；而带显式forall注解的 lambda 不能像普通 lambda 一样被自由改写——若浮动过程丢失了注解，lambda 的类型就会从"对任意r可用"退化为"只能用于某个具体r"，从而产生类型错误的程序。该测试用例正是把这一敏感场景固化下来：只要编译器在浮动时错误地剥离或改写注解，下面的期望输出就会失配，测试随即失败。

三、期望输出：浮动后注解语义必须保留

foo定义提交后，transcript 通过display foo命令展示其规范化形式，期望输出为：

> display foo x -> bar (f -> f x)

这里有两个观察点：

• display foo得到的仍是x -> bar (f -> f x)，说明bar的参数(f -> f x)作为一个完整的 lambda 得以保留，没有被错误的浮动过程拆散或替换；
• 打印结果中不显示: forall r. (a -> r) -> r注解，是因为展示层会省略可由类型推导补全的注解；但"省略展示"不等于"丢失注解"。内部表示中该 lambda 仍被标记为带注解，编译器随后的类型检查、哈希与 ANF 变换均依赖这一点。

四、源码级原理：注解与浮动在 ANF 中的处理

要理解为什么这个用例能卡住缺陷，需要回到 Unison 运行时库的 ANF 变换实现 unison-runtime/src/Unison/Runtime/ANF.hs。

1. 带注解 lambda 的模式：LamsAnnot与Ann'

ANF 变换中，带注解的 lambda 由模式LamsAnnot vs0 mty vs1 body表示（vs0为前置参数、mty为可选的返回类型注解、vs1为后续参数、body为函数体），而独立的类型注解项则由Ann' tm ty表示。unAnn、unLamsAnnot等辅助函数（ANF.hs）负责在遍历时识别并剥离/保留这些结构。

2.floater：浮动变换的入口

浮动逻辑的核心是floater函数（ANF.hs）。它对不同类型的项给出不同的处理：

floater top rec tm0@(Ann' tm ty) = (fmap . fmap) (\tm -> ann a tm ty) (floater top rec tm)

• 对于Ann' tm ty，它先递归浮动内部项tm，再把注解ty原样包回去——这正是"浮动不能丢失注解"的实现保障；
• 对于LamsAnnot vs0 mty vs1 bd，在非顶层时（otherwise分支），它会进入inLocalLam局部作用域递归处理函数体，并通过lamFloater True tm Nothing a (vs0 ++ vs1) bd将 lambda 提升为新的命名变量lv，然后把原位置替换为对该变量的引用（var a lv）。

3. 被浮动 lambda 的命名：Var.Float

被浮动的 lambda 需要一个全新的内部变量名。在 unison-core/src/Unison/Var.hs 中，变量类型Var.Type明确声明了一个专用于此的构造子：

| -- An unnamed variable for a floated lambda Float

其rawName渲染为_float，与Eta（_eta）、ANFBlank（_anf）、Pattern（_pattern）等其他编译器内部变量并列。ANF.hs 中的nameLambda与freshFloat（ANF.hs）负责为被浮动的 lambda 分配不冲突的新名字，FloatState中的floated列表则记录已浮动的绑定，供后续重命名与替换使用。

4. 自由变量追踪：keep集合

浮动还必须正确追踪自由变量。enclose系列函数（ANF.hs）维护一个keep集合，用于记录"将要被提升、因此必须保留的变量"。例如对Let1NamedTop'且绑定体为 lambda 的项，会先把该变量v加入keep，再递归处理。对于LamsAnnot，其处理逻辑是：

enclose keep rec t@(LamsAnnot vs0 mty vs1 body) = Just $ if null evs then lamb else apps' lamb $ map (var a) evs where keep' = Set.difference keep $ Set.fromList (vs0 ++ vs1) fvs = ABT.freeVars t evs = Set.toList $ Set.difference fvs keep ... lamb = lamsAnnot a (evs ++ vs0) mty vs1 lbody

其中evs是函数体自由变量减去keep后的剩余部分——这些变量必须被抽取为外层 lambda 的参数，同时构造 lambda 时仍调用lamsAnnot保留原来的mty注解。这条路径正是本测试用例所守护的代码：任何一步忘记把注解传下去，都会让foo的display结果偏离预期。

5. 术语层的对应关系

在语法树层面，unison-core/src/Unison/Term.hs中术语构造子也包含对应的Ann（带类型注解的项）与Lams（多参数 lambda）形式，ANF 变换正是在Term的 ABT 表示之上工作的。可以说，本测试从"用户可感知的展示输出"这一端，反向约束了从 Term.hs 到 ANF.hs 整条编译链路上注解的传递完整性。

五、如何运行与验证这个测试

该文件属于unison-src/transcripts/idempotent/下的幂等 transcript，无需单独执行，会随 transcript 测试套件一起被运行：

1. 构建 UCM 后，运行 transcript 测试（仓库根目录下通常通过cabal/stack的测试目标驱动，入口见 unison-cli/transcripts/Transcripts.hs）；
2. transcript 运行器会解析fix-annotated-lambdas.md中的代码块：
   • 第一段ucm :hide块执行builtins.merge，把内置类型与函数合并进临时代码库（:hide表示隐藏这段交互输出）；
   • 第二段unison块定义foo与bar，并回填 UCM 的 add 结果，其中bar被报告为(∀ r. (a -> r) ->{g} r) ->{g} a、foo为a -> a，说明在{g}能力集上下文下类型检查通过；
   • 第三段ucm块执行> display foo，期望输出x -> bar (f -> f x)；
3. 若实际输出与该文档中的期望输出不一致，即视为回归（说明浮动逻辑再次破坏注解语义）。

六、小结

fix-annotated-lambdas.md篇幅虽短，却是 Unison 编译器质量保障体系中的一个精确探针：它以最小化的 Rank-2 多态代码，锁定了"带forall注解的 lambda 在 ANF 浮动阶段不得丢失注解"这一不变量。结合 unison-runtime/src/Unison/Runtime/ANF.hs 中floater/enclose/lamFloater的实现与 unison-core/src/Unison/Var.hs 中Var.Float的命名约定，读者可以清晰地看到：一个看似简单的display输出，背后是注解重建（Ann'回包）、注解保持（lamsAnnot透传mty）、自由变量抽取（keep集合）三者协同工作的结果。这正是"以输出约束实现"的回归测试范式的典型体现。

• 编程语言
• 编译器
• 语言运行时
• 开发工具