adapter 设计

设计目标

下游仓库有自己的 AST（多项式表达式、数值表达式树、带类型的核心语言），不应为了获得正确的绑定语义而必须把它们转换为 Term[T]。adapter 设计规定了这样的 AST 如何通过 @syntax.BindingSyntax 接入共享算法、实现必须保证什么，以及如何测试这一保证。adapter 包包含参考契约测试；它没有公共 API。

数学背景

视图

设 $N$ 为下游 AST，并设

F(X) = 1 + \mathcal{N} + X \times X^{*} + \mathcal{N} \times X

为绑定语法的签名函子，其和项为 BindingView[X] 的 Opaque、Variable、Apply 和 Bind。一个 adapter 由一个投影（余代数）和若干构造子（部分代数）组成：

\pi : N \to F(N) \quad (\texttt{project}), \qquad \kappa : F(N) \setminus 1 \to N \quad (\texttt{variable},\ \texttt{apply},\ \texttt{bind}).

视图定律

对所有名 $x$ 、节点 $h, b, n$ 和数组 $\bar a$ ：

\begin{aligned} \text{(V1)}\quad & \pi(\kappa(\mathsf{Variable}(x))) = \mathsf{Variable}(x), \\ \text{(V2)}\quad & \pi(\kappa(\mathsf{Apply}(h, \bar a))) = \mathsf{Apply}(h, \bar a), \\ \text{(V3)}\quad & \pi(\kappa(\mathsf{Bind}(x, b))) = \mathsf{Bind}(x, b), \\ \text{(V4)}\quad & \pi(n) \ne \mathsf{Opaque} \implies \kappa(\pi(n)) \equiv n, \\ \text{(V5)}\quad & \pi(n) = \mathsf{Opaque} \implies n \text{ contains no variable occurrence}, \\ \text{(V6)}\quad & \pi(n) = \mathsf{Apply}(h, \bar a) \text{ or } \mathsf{Bind}(x, h) \implies h, a_i \text{ are smaller than } n. \end{aligned}

(V1)–(V3) 说的是构造子构建出的正是投影所报告的内容；(V4) 说的是重建一个被投影的节点会得到等价的节点（ $\equiv$ 是下游的相等概念，通常是 ==）；(V5) 是 Opaque 的“闭原子”契约；(V6) 使经由 $\pi$ 的结构递归终止。在 (V1)–(V4) 下， $\pi$ 限制在非 opaque 节点上与 $\kappa$ 互逆，因此去掉 opaque 节点后的 $N$ 同构于 $N$ 之上的一层绑定语法。

为什么这些定律就足够了

每个泛型算法都通过经由 $\pi$ 的结构递归定义，并用 $\kappa$ 重建。对每个算法，syntax 和 substitution 设计中关于 Term[T] 的定律证明恰好用到 Term 的两个事实：模式匹配能看到构造子，以及构造子构建的正是这些节点。(V1)–(V4) 对 $N$ 陈述了这些事实。(V5) 证明了把 opaque 节点视为 $\mathrm{FV} = \mathrm{names} = \varnothing$ 的合理性，(V6) 给出良基归纳。因此，对于合法的 adapter：

generic_free_variables 和 generic_all_names 计算把节点读作绑定语法时的 $\mathrm{FV}$ 和 $\mathrm{names}$ ；
generic_alpha_rename_bound 满足 alpha 步；
GenericSubstitution::apply_once 是同时且避免捕获的（substitution 设计的引理 1–3）；
generic_top_down_once 满足 rewrite 设计中的单可约式契约和范式引理。

设计决策

用视图 trait 而非转换

问题。 下游 AST 可以先转换为 Term[T]，处理后再转换回来。

选项。 转换函数；泛型遍历库（带 map 的函子）；视图 trait。

选择。 一个带有一个投影和三个构造子的视图 trait。与转换不同，它只分配算法重建的节点，并保留下游的节点种类：被投影为 Apply 的求和节点会被重建为求和节点，而不是应用。与一般的函子不同，它不需要 MoonBit 所没有的高阶类型：视图是具体类型 BindingView[N]。

视图只区分绑定所需的东西。含有和、积与幂的下游 AST 可以把三者都投影为 Apply；此时构造子 apply(head, args) 必须重建出正确的种类，而这只有在种类可以从 head 或参数中恢复时才能做到。契约测试中的求和节点是最简单的情形：只有一种类似 Apply 的节点。当需要重建多种节点时，把运算符编码在头部（例如作为 opaque 运算符节点），使 (V4) 成立。

Opaque 节点是原子

Opaque 节点原样返回，且从不在其中查找变量。这与 Term[T] 中 Value(T) 的契约相同，正是它让任意类型的字面量（整数、浮点数、有理数）无需自己的 trait 就能参与进来。确实包含变量的节点不得投影为 Opaque（V5）；否则代换会悄无声息地跳过这些变量。

领域策略留在下游

该 trait 只提供绑定结构。规范形式、运算符求值、化简顺序和不动点迭代都是由下游包通过 rewrite 提供的规则和策略；底层库不固定其中任何一项。这使库不依赖于任何特定代数，并让每个下游包各自记录自己的策略。

桥接变量类型

下游变量类型通过单射（不同变量映射到不同名）转换为 @core.Name。正是单射性使名的相等与变量的同一性一致，从而对下游变量而言新鲜性和捕获检查是正确的。

正确性 / 不变量

契约测试 src/adapter/poly_adapter_wbtest.mbt 针对一个有四种节点的 AST 检查一个合法的 adapter：

性质	检查
同时的单遍代换	$\{x \mapsto y, y \mapsto 2\}$ 作用于 $x + y$ 得到 $y + 2$
未映射的变量保持不变	$\{x \mapsto 3\}$ 作用于 $x + y$ 得到 $3 + y$
重写通过构造子重建	在路径 `[ApplyArgument(0)]` 处 $1 + (0 + 2) \to 1 + 2$

下游 adapter 应为自己的节点种类添加 (V1)–(V5) 的测试：投影每个构造子的结果，重建每个被投影的节点，并检查 opaque 节点没有自由变量。

被否决的替代方案

让 Term[T] 成为唯一的 AST。 被否决，因为下游 AST 携带 Term[T] 无法表达的不变量（范式化的系数、带类型的节点）。
带有 sort 或多元绑定子的更大视图。 更多分支会使每个 adapter 和每个泛型算法都变得更大；嵌套的 Bind 节点就能表达多元绑定子。
在运行时检查定律。 这些定律是关于所有节点的等式；它们通过测试验证，而非强制执行。

边界

该 trait 无法表达作用域不是单个子节点的绑定子，也无法表达在不同子节点中绑定多个名的节点。
合法性由实现者负责；不合法的 adapter 从泛型算法得到的结果是未定义的。
adapter 包不导出任何内容；它只测试契约。