Haskell 如何处理类型的 Alpha 等价比较？

结论

不能让同一个 Eq 实例只对部分构造器使用自定义逻辑，同时对其他构造器自动回退到 deriving Eq。派生的 Eq 实现会递归调用字段的相等判断，因此为 SType 手写 Eq 时，必须明确处理每个构造器。

一种更稳妥的做法是先把绑定变量转换成规范表示，再进行比较。例如，将 ∀α. α → α 和 ∀β. β → β 中的绑定变量都表示为“距离当前绑定点为 0 的变量”，然后为规范表示派生 Eq。自由变量仍按名称比较。

示例：先转换成规范表示

题目省略了 9 个构造器。下面用 SForall 表示全称量词，只展示 SInt、SBool、SVar、SArrow 和 SForall 的处理方式。实际使用时，还需要为其他可能包含子类型或绑定变量的构造器补上相应的转换规则。

import Data.List (elemIndex)

data SType
  = SInt
  | SBool
  | SVar String
  | SArrow SType SType
  | SForall String SType
  deriving (Show)

data CanonicalType
  = CInt
  | CBool
  | CFree String
  | CBound Int
  | CArrow CanonicalType CanonicalType
  | CForall CanonicalType
  deriving (Eq, Show)

canonicalize :: SType -> CanonicalType
canonicalize = go []
  where
    go boundVars ty = case ty of
      SInt -> CInt
      SBool -> CBool
      SVar name -> case elemIndex name boundVars of
        Just index -> CBound index
        Nothing    -> CFree name
      SArrow left right -> CArrow (go boundVars left) (go boundVars right)
      SForall name body -> CForall (go (name : boundVars) body)

alphaEquivalent :: SType -> SType -> Bool
alphaEquivalent a b = canonicalize a == canonicalize b

boundVars 按绑定变量离当前位置由近到远排列。因此，遇到 SForall name body 时，将 name 放到列表头部。引用绑定变量时，elemIndex 返回的索引就是它距离最近绑定点的层数。若名字不在绑定列表中，它会保留为 CFree name，因此不同的自由变量仍不相等。

例如，用 SForall "α" ... 和 SForall "β" ... 分别表示 ∀α. α → α 与 ∀β. β → β，两者规范化后都会包含 CForall (CArrow (CBound 0) (CBound 0))，所以比较结果为 True。

为什么不建议在手写 Eq 中回退到 ==

如果 Eq SType 对 SForall 使用 Alpha 等价判断，却对 SArrow 或其他构造器使用普通的 ==，那么这些构造器中嵌套的类型仍会按变量名比较。相等判断需要递归使用同一套绑定规则，否则外层或内层的 Alpha 等价都可能被漏掉。

上例将相等判断放在独立的 alphaEquivalent 函数中，并为 CanonicalType 派生 Eq。这样，派生的相等判断只用于已经规范化的结构，不会绕过 Alpha 等价规则。

另一种做法：直接使用 de Bruijn 索引

如果可以调整类型表示，也可以在解析或构造类型时就把绑定变量存为 de Bruijn 索引，并将自由变量单独存为名称，例如 Bound 0 和 Free "x"。这样，Alpha 等价的变量会自然得到相同的索引，之后只需为类型结构派生 Eq。如果实现中需要频繁比较类型，这种方式通常更直接。

无论选择哪种方式，都需要明确绑定作用域、变量遮蔽和自由变量的比较规则。如果 SType 中没有表示全称量词或其他绑定结构的构造器，仅凭变量名称无法判断变量是否受绑定，也就无法正确实现 Alpha 等价。

备注：内容仅供参考。