一致性与孤儿实例规则
摘要
本文解释了类型类系统中一致性的概念,并讨论了编程语言中的孤儿实例规则,以Haskell和Rust为例。
<p><a href="https://lobste.rs/s/vbu5ay/coherence_orphan_instance_rules">评论</a></p>
查看缓存全文
缓存时间: 2026/09/01 13:40
# 一致性与孤儿实例规则
来源:https://osa1.net/posts/2026-08-29-coherence-and-orphans.html
**2026年8月29日** - 标签:[en](https://osa1.net/tags/en.html),[haskell](https://osa1.net/tags/haskell.html),[rust](https://osa1.net/tags/rust.html),[plt](https://osa1.net/tags/plt.html)。
类型类是一种重载机制,允许编译时或运行时多态。像 `m a b ...`(或 Rust 中的 `a.m(b, ...)`)这样的类型类方法调用会根据传递给方法的类型参数解析为具体方法。
```haskell
class ToString t where
toString :: t -> String
instance ToString Bool where
toString = undefined
instance ToString Int where
toString = undefined
f = toString (123 :: Int)
g = toString True
```
这里的 `toString` 是被重载的:两次对同一方法的调用实际上调用的是不同的具体方法。
这些类型参数通常基于参数或返回值(从调用上下文推断)。
```haskell
class Convertible a b where
convert :: a -> b
instance Convertible Int String where
convert = show
instance Convertible Int Bool where
convert = (/= 0)
f :: Bool
f = convert (123 :: Int) -- 实际调用的方法取决于返回类型
```
当类型类类型参数未在方法签名中使用时,编译器无法选择实例,因此我们必须显式指定类型参数:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
class Ambiguous a b where
weird :: a -> IO ()
instance Ambiguous Int Bool where
weird _ = putStrLn "First instance"
instance Ambiguous Int String where
weird _ = putStrLn "Second instance"
f :: IO ()
f = weird @Int @Bool (123 :: Int)
```
这里 `f` 调用的是 `Ambiguous Int Bool` 的 `weird`,基于显式类型参数。没有类型参数,编译器无法知道调用哪个 `weird`。
关键在于,实例不是一等值,也没有名称。这有助于保持我们在处理类型类时希望具有的一个有用属性:如果我们在程序的不同部分用相同的类型参数调用同一方法,它们都应调用同一方法。这一点至关重要,如果你曾使用 Rust 的 traits 或 Haskell 的类型类编程过,即使时间很短,你也必然编写过依赖此属性的代码。
我们依赖此属性的一些常见情况包括:
- 如果我们用重载函数记录/打印一个值,对于相同参数的打印格式是相同的,无论它在何处被打印。
- 如果我们在程序的一部分(例如库 A)中序列化一个值,然后在另一部分(例如库 B)中反序列化它,序列化和反序列化调用点使用相同的实例,因此它们期望的格式是兼容的。
- 对于基于 `Hash` 和 `Ord` 的数据结构(例如哈希或有序映射和集合),插入和查找点始终使用相同的哈希码函数,从而维护数据结构不变式,并且例如永远不会添加重复的键等。
这个属性被称为**一致性**。
(如果你熟悉带有子类型的面向对象编程,一致性在面向对象语言中也存在:对于相同类型的 `x`,`x.m()` 在程序的任何地方都调用相同的方法 `m`。)
更正式地说,一致性指出,对于任何约束 `C type1 ... typeN`,最多只能有一个匹配该约束的实例。因此,如果一个方法调用生成了该约束,我们知道最多只有一个实例匹配该约束,并且将调用该实例的方法。
当存在多个可能匹配同一约束的实例时,它们被称为**重叠**实例。重叠实例是导致系统不一致的途径。
关于一致性的一个重要事实是它是一个全局(或整个程序)属性。如果没有全局性地声明一个约束最多只能解析到一个实例,程序的不同部分(可能是不同的库、模块)可能会出现例如 `Hash String` 解析到不同实例的情况,从而破坏我们的数据结构不变式。
(用面向对象术语来说,你可以将其想象为对于完全相同的 `x`,`x.hashCode()` 在程序的不同部分返回不同的值,并且在此期间 `x` 没有被修改。)
下面是一个模块自身一致,但导入它们的主模块不一致的例子:
```haskell
-- C.hs
class C a b
-- A.hs
import C
data A = A
instance C A b
-- B.hs
import C
data B = B
instance C a B
-- Main.hs
import C
import A
import B
test :: C p q => p -> q -> IO ()
test _ _ = pure ()
main = test A B
```
这里 `A` 和 `B` 各自是一致的,但 `Main` 不是,尽管它没有定义任何实例。在 `Main` 中,`C A B` 被导入的两个实例都匹配了。
一致性作为全局属性带来了挑战。我们希望库能够组合。如果我们接受两个库(如上面的 A 和 B)是类型安全且一致的,那么我们应该能够在第三个库中导入它们,并且系统仍然保持一致。否则,如果我们也考虑传递依赖,就会产生一个碎片化的库生态系统,许多库无法在同一程序中直接或间接地使用。
这由**孤儿实例规则**来保证。这些规则限制我们可以在哪里定义实例,目标是确保一致的库可以被组合。
对于这篇博文的目的来说,确切的规则并不重要(它们也取决于语言)。然而,作为一个例子,如果我们上面的 `C` 是单参数版本,并且另一个库中有一个类型:
```haskell
-- C.hs
class C a
-- A.hs
data A = A
```
孤儿实例规则规定 `instance C A` 唯一可以放置的地方是在 `A.hs` 中。因此,不可能有两个定义 `instance C A` 的模块都能在第三个模块中被导入,该实例只能来自 `A`。
那么双参数版本 `class C a b` 呢?允许像以下这样的实例的规则会是什么:
- `instance C A b`
- `instance C a B`
- `instance C A B`
- `instance C [a] b`
- `instance C a (Maybe b)`
- ...
或者,如果我们在类中还有更高种类的类型参数,比如 `Foldable` 呢?如果我们还有额外的类型参数呢?
制定模块化的规则以强制执行全程序一致性,同时又不至于过于严格(允许常见和有用的用例)是一个不简单的问题。例如,在 Rust 中,上面不一致的 Haskell 示例是不允许的:实例 `instance C a B` 被孤儿实例规则禁止。禁止此实例的规则细节在一个名为“Re-rebalancing coherence”的 RFC 中有描述 (https://github.com/rust-lang/rfcs/pull/2451)。但请注意:
1. 这是对早期孤儿实例规则变更“Rebalancing coherence”的后续 (https://github.com/rust-lang/rfcs/pull/1023),该变更被证明过于严格。
2. 新规则是健全的(即,如果允许两个库中的两个实例,那么第三个导入这两个库的库不会变得不一致)这一点并不完全明显(至少对我来说是这样)。
根据定义,孤儿实例规则需要遵循实例解析(或约束求解)规则:我们希望一个约束在整个程序中解析到一个实例(如果它能解析的话)。随着实例解析规则的不同,孤儿规则也必须相应改变。
然而,有趣的是,我未能找到任何对孤儿实例规则的形式化处理,带有证明这些规则只允许一个一致系统以及它们支持的常见用例示例。我认为这里有一个语言设计研究机会:我们可以形式化实例解析规则和孤儿实例规则,并证明这些规则只允许一个全局一致的系统。
关于实例解析和孤儿规则还有很多要说的,所以希望以后能有更多关于这个主题的内容。在这篇文章中,我只是想给出一些定义,我将在后面引用它们。
相似文章
揭秘类型(及一些悖论的解惑)
类型理论为编程语言基础增加了不必要的复杂性,并提出基于关系成员的更简单观点。
类型系统中的反例 (2021)
一个精心收集的反例合集,展示了类型系统的局限性和陷阱,作为程序员和语言设计者的教育资源。
记录类型推断入门指南
本文解释了静态类型语言中匿名记录类型推断的基础知识,使用了类型理论符号并以Haskell作为实现语言。
遵从性 vs 理解
作者回顾了他在软件标准和开源领域的职业生涯,然后描述了使用 Claude 构建一个名为 Roundhouse 的编译器,该编译器将 Rails 应用程序转换为静态类型语言,如 Rust、Crystal 和 TypeScript。
Stroustrup法则(2024)
Bjarne Stroustrup的法则指出:对于新特性,程序员更偏好显式语法,但一旦该特性被确立,他们就更倾向于简洁表示法。本文探讨了 Rust 和 Python 中的示例,并讨论了这对语言设计和教学的影响。