类型类的字典传递翻译

源接口的“需要Eq a”像一个隐藏的工具参数。翻译把工具摆到桌面上：你调用member时，除了要找的值和列表，还交来一把相等比较工具。member不再猜元素到底是整数还是字符串，只调用这把工具。

列表相等不是另一种神秘的运行时类型检查。它接收元素相等工具，然后生成一把逐项比较列表的工具。嵌套列表便是工具构造器的嵌套应用。

member的完整字典接口 ​

源程序为

member : ∀a. Eq a ⇒ a → List a → Bool
member x []      = false
member x (y::ys) = eq x y || member x ys

翻译后写成

memberD : ∀a. EqDict a → a → List a → Bool
memberD = Λa. λ(d : EqDict a). λ(x : a). λ(xs : List a).
  match xs with
  | []      -> false
  | y :: ys -> d.eq x y || memberD[a] d x ys

递归调用显式传回同一个d。由于该函数递归访问同一种元素类型，无须在每层重新搜索实例。d.eq:a→a→Bool，所以方法调用和递归分支都是Bool；字典参数把源条件的使用变成了普通类型检查。

整数实例是

intEq : EqDict Int
intEq = { eq = λ(x:Int). λ(y:Int). integerEqual(x,y) }

列表实例构造器为

listEq : ∀a. EqDict a → EqDict (List a)
listEq = Λa. λ(d : EqDict a).
  { eq = let rec same xs ys =
           match (xs,ys) with
           | ([],[])             -> true
           | (x::xt,y::yt)        -> d.eq x y && same xt yt
           | ([],_::_) | (_::_,[]) -> false
         in same }

长度不同时的两个分支不可省略。递归每次同时缩短两个非空列表，故对有限列表终止；比较到首个不相等元素时也可短路退出。

一次具体字典构造与执行 ​

源调用 member [2,4] [[1],[2,4]]要求Eq(List Int)。编译时解析出证据 listEq[Int] intEq，得到

memberD[List Int] (listEq[Int] intEq) [2,4] [[1],[2,4]]

执行依次比较 [2,4]与[1]，首元素2与1不等，得到false；再比较 [2,4]与[2,4]，元素2、4分别相等，最后两个空尾相等，得到true。外层member返回true。类型层的List Int决定需要哪种字典，运行时字典的方法执行普通列表递归。

为什么两个字典会改变意义 ​

对Int再定义另一份合法方法记录：

parityEq = { eq = λx. λy. (x mod 2) == (y mod 2) }

memberD[Int] intEq 3 [1]返回false，memberD[Int] parityEq 3 [1]返回true。两份记录的类型都正确，甚至各自都给出一个等价关系；类型并不要求它们是同一个比较。

显式字典语言允许这种区别，因为调用者明白地选择了参数。但源语言若在同一个 Eq Int目标上偷偷任选字典，同一表达式的不同推导就会有不同结果。因此，无重叠、无歧义与一致的证据选择是语义责任，不仅是让实例搜索快一点的工程约定。

类的代数规律也不会仅由字典字段类型自动证明。若一个类要求比较满足某些额外法律，应把它们作为实例的独立规范；翻译只把操作与已有证据显式化。

类型正确性的证明沿源推导归纳。普通变量、应用和λ保持原结构；约束引入对应增加字典λ；约束消去对应应用已经构造且类型正确的字典；方法出现对应记录投影。这给出编译翻译公理库语义保持的编译器阶段Semantics-preserving compiler pass · Correct compiler transformation · 编译阶段语义保持在固定观察、错误与未定义行为契约下，要求一次编译变换的目标程序不产生源程序未允许的行为。的一半责任：源程序可导出时，译后程序具有对应核心类型。

另一半是运行含义。源重载操作的语义必须由所选实例方法规定，目标用投影和β归约执行同一个方法。固定规范证据时，可以按求值步或求值推导证明两边对应。一致性还要求不同合法类型推导产生的译文具有相同可观察行为；这不是“每个译文都类型正确”的同义词。

在本页受限实例系统中，具体目标由唯一、结构递减的实例链构造，局部前提又复用指定字典；配合无歧义接口，可以避免前例那种隐式选择分歧。若后来加入重叠、局部实例、超类多路径或显式证据转换，需重新说明怎样维持证据一致性。

翻译的成本应与实例搜索分开计。若类型推导及每次使用的证据树已经给定，设它们按出现次数计的总大小为N，逐节点生成类型抽象、字典参数、应用和投影需要 $O(N)$ 时间，显式目标树也有 $O(N)$ 大小。若输入证据以共享DAG保存，并在目标中用绑定保留共享，可按节点和边数线性生成；反复内联同一证据会展开共享，成本应按展开后的大小计。寻找实例、检查条件及发现歧义的工作发生在此前，不能从这份翻译成本中抹掉。

译后memberD逐项扫描外列表，至首个匹配或列表末尾停止。若共比较k项，每次字典比较成本为cᵢ，则时间为 $O(1+k+\sum _{i=1}^k{c}_i)$。listEq对两个长度为m、n的列表同步扫描；元素比较为常数成本时，最坏时间为 $O(min(m,n)+1)$，最后的加一覆盖空尾或长度不等检查。这里讨论的是逐节点的模式匹配实现，不先各自遍历一遍求长度。额外空间取决于求值器：直接递归可能保存线性深度的调用帧，支持相应尾调用/短路编译的实现可让这段扫描使用常数额外栈；字典本身及输入列表的存储另计。

字典传递使实现策略可见：运行时可以传一个记录指针，也可以在已知实例处内联方法或做特化。但删除字典分配、移动求值或展开递归仍要保持原语言的效果与终止行为；源类型类条件不会自动授权任意优化。