受约束类型方案

参数多态的member不能凭空比较两个未知类型的值。它需要一项能力：“给定两个a，返回它们是否相等。”把这项要求留在接口中，既不强迫member只服务Int，也不假装所有类型都天然支持相等比较。

约束会跟着使用传播。内部调用eq产生Eq a条件，外部定义若无法自行消除，就把条件放入自己的方案。最终使用具体类型时，实例解析再寻找所需证据。

从函数体收集member的条件 ​

定义

member x xs =
  match xs with
  | []       -> false
  | y :: ys  -> eq x y || member x ys

列表匹配要求xs:List a，并给出y:a、ys:List a。eq x y把x也约束为a，并产生Eq a条件；递归调用仍在同一个a上，要求相同条件，不增加新类。

由类型等式合一公理库一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。得到形状 $a\to \mathrm{List}(a)\to \mathrm{Bool}$；由约束传播得到P={Eq a}。a不自由出现在外层环境中，因而最终方案为

member 3 [1,3]把a实例化为Int，待解条件Eq Int由注册实例直接满足。member [3] [[1],[3]]把a实例化为List Int，解析依次为

如果输入是函数列表，而实例环境没有Eq(Int→Int)，就留下无法解决的约束。类型形状可能完全一致，错误仍来自操作能力缺失。系统不会由函数类型相同自动生成函数相等算法。

未知条件可以合法保留 ​

在有假设Eq a的函数体内使用member，不需要把a马上确定为某个具体类型；直接复用假设即可。只有当一个闭合可执行程序仍留下无来源的字典需求时，才必须报告未解决条件。

这与HM公理库Hindley–Milner 类型推断Hindley–Milner type inference · HM type system为带 let 的秩一参数多态 λ 演算提供主类型性质与可判定类型推断的系统。的扩展关系很清楚：普通形状等式仍用合一处理，操作约束则交给另一套蕴涵/实例规则。不要把Eq a当作又一个需要与Int合一的类型表达式。

歧义不等于“还没想好显示什么类型” ​

设有

表达式 fun s -> show (read s)可以收集到

a只出现在条件里，不出现在输入输出形状中。调用者传一个字符串，无法由通常的类型实例化确定选择哪套Read/Show证据。

为看到这会影响含义，给定两组具体实例：Int的read把十进制文字解析成整数，show输出无前导零的十进制；另有Token类型，其read保存输入文字，show原样返回。输入"007"在第一组得到"7"，在第二组得到"007"。这不是可随意忽略的搜索顺序区别。

在本页无默认化系统中，采用简单无歧义条件

来拒绝这种暴露在接口上的选择。给中间结果注明Int，或显式传入解析/打印操作，都能使意图确定。更丰富的系统可能使用函数依赖、默认化等规则，那是另外声明的消歧机制，不能暗中假定。

实例解析是否终止需要单独保证。上面的列表规则每次把目标Eq(List T)缩成Eq T，类型构造器数量严格减少，因此有限嵌套列表最终到达基本类型。若允许 Eq a⇒Eq a或不受约束地使目标越变越大，就不能再据此保证终止。

无重叠意味着一个具体目标不会同时匹配两条不同实例头；有限、结构递减的规则又使搜索可以结束。这些简单纪律足以让本页的小系统可预测，但通用qualified-types框架本身并不自动附带可判定的蕴涵器或唯一实现。

类型约束还有可执行解释。字典传递翻译公理库类型类的字典传递翻译Type class dictionary passing · Dictionary translation把类型类条件编译为方法记录参数，并区分译后类型正确与不同证据选择的语义一致性。把Eq a变成一个普通参数，里面装着相等方法；列表实例则是把元素字典变成列表字典的构造函数。于是“条件如何证明”与“运行时使用哪个操作”接到一起，也解释了为什么歧义和重叠会影响程序语义。