为什么 Haskell 说这是模棱两可的？

Question

我有一个这样定义的类型类：

class Repo e ne | ne -> e, e -> ne where
  eTable :: Table (Relation e)

当我尝试编译它时，我得到了这个：

* Couldn't match type `Database.Selda.Generic.Rel
                             (GHC.Generics.Rep e0)'
                     with `Database.Selda.Generic.Rel (GHC.Generics.Rep e)'
      Expected type: Table (Relation e)
        Actual type: Table (Relation e0)
      NB: `Database.Selda.Generic.Rel' is a type function, and may not be injective
      The type variable `e0' is ambiguous
    * In the ambiguity check for `eTable'
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        eTable :: forall e ne. Repo e ne => Table (Relation e)
      In the class declaration for `Repo'
   |
41 |   eTable :: Table (Relation e)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

我希望一切都是明确的，因为我已经明确指出 e 决定 ne，反之亦然。

但是，如果我尝试像这样定义我的类只是为了测试目的，它会编译：

data Test a = Test a
class Repo e ne | ne -> e, e -> ne where
    eTable :: Maybe (Test e)

我不太确定导致这种情况的 Table 和 Relation 类型是怎么回事。

Answer 1

Test 是单射的，因为它是一个类型构造函数。

Relation 不是单射的，因为它是一个类型族。

因此模棱两可。

愚蠢的例子：

type instance Relation Bool = ()
type instance Relation String = ()

instance Repo Bool Ne where
   eTable :: Table ()
   eTable = someEtable1

instance Repo String Ne where
   eTable :: Table ()
   eTable = someEtable2

现在，eTable :: Table () 是什么？它可能是来自第一个或第二个实例的那个。这是模棱两可的，因为Relation 不是单射的。

Answer 2

歧义的来源实际上与 ne 没有在类中使用（您通过使用函数依赖项来解决）无关。

错误信息的关键部分是：

  Expected type: Table (Relation e)
    Actual type: Table (Relation e0)
  NB: `Database.Selda.Generic.Rel' is a type function, and may not be injective

请注意，匹配时遇到问题的是 e，而 NB 消息会引起您对类型函数和注入性问题的注意（您确实必须知道这一切意味着什么消息才能有用，但是它包含您需要查找的所有术语以了解正在发生的事情，因此它非常适合编程错误消息）。

它抱怨的问题是类型构造函数和类型族之间的关键区别。类型构造函数总是单射的，而一般的类型函数（尤其是类型族）不一定是。

在没有扩展的标准 Haskell 中，构建复合类型表达式的唯一方法是使用类型 构造函数，例如 data Test a = Test a 中的左侧 Test。我可以将Test（类型为* -> *）应用于Int（类型为*）以获取类型Test Int（类型为*）。类型构造函数是injective，这意味着对于任何两个不同的类型a 和b，Test a 是与Test b 不同的类型¹。这意味着在类型检查时您可以“向后运行”；如果我有两种类型t1 和t2，它们都是应用Test 的结果，并且我知道t1 和t2 应该相等，那么我可以“取消应用”@987654342 @ 获取参数类型并检查它们是否相等（或推断其中一个是什么，如果它是我还没有弄清楚而另一个是已知的，等等）。

类型族（或任何其他形式的不知道是单射的类型函数）不向我们提供这种保证。如果我有两种类型 t1 和 t2 应该相等，并且它们都是应用一些 TypeFamily 的结果，那么就无法从结果类型转到 TypeFamily 的类型应用于。特别是，没有办法从TypeFamily a 和TypeFamily b 相等这一事实得出结论，a 和b 也相等；类型族可能恰好将两种不同的类型a 和b 映射到相同的结果（injectivitiy 的定义 是它不这样做）。因此，如果我知道a 是哪种类型但不知道b，知道TypeFamily a 和TypeFamily b 是相等的并不会给我更多关于b 应该是什么类型的信息。

不幸的是，由于标准的 Haskell 只有类型构造函数，Haskell 程序员受过良好的训练，只是假设类型检查器可以通过复合类型向后工作以连接组件。我们通常甚至没有注意到类型检查器需要向后工作，我们已经习惯于只查看具有相似结构的类型表达式并跳到明显的结论而无需完成所有步骤类型检查器必须通过。但是因为类型检查是基于计算出每个表达式的类型，包括自下而上² 和自上而下³ 并确认它们是一致的，类型检查表达式的类型涉及类型族很容易遇到模棱两可的问题，在我们人类看来它“显然”没有模棱两可。

在您的Repo 示例中，考虑类型检查器将如何处理您使用eTable 的位置，例如(Int, Bool) 对应e。自上而下的视图将看到它在需要一些Table (Relation (Int, Bool)) 的上下文中使用。它将计算Relation (Int, Bool) 的计算结果：假设它是Set Int，所以我们需要Table (Set Int)。自下而上的传递只是说eTable 可以是Table (Relation e) 任何e。

我们使用标准 Haskell 的所有经验都告诉我们，这很明显，我们只需将 e 实例化为 (Int, Bool)，Relation (Int, Bool) 再次计算为 Set Int，我们就完成了。但实际上它不是这样工作的。因为Relation 不是单射的，所以e 可能有其他选择，这给了我们Set Int 和Relation e：也许Int。但是如果我们选择e 为(Int, Bool) 或Int，我们需要寻找两个不同的Repo 实例，它们对于eTable 将有不同的实现，即使它们的类型是一样的。

即使每次使用 eTable 时添加类型注释（如 eTable :: Table (Relation (Int, Bool))）也无济于事。类型注解只会向自顶向下视图添加额外信息，而我们通常已经拥有这些信息。类型检查器仍然遇到这样一个问题：e 与 (Int, Bool) 相比可能存在（无论是否实际存在）其他选择，这导致 eTable 匹配该类型注释，所以它不知道哪个要使用的实例。 任何可能使用eTable 都会出现此问题，因此在定义类时会报告为错误。这基本上是出于同样的原因，当你有一个类的某些成员的类型不使用类头中的所有类型变量时，你会遇到问题。您必须考虑“仅在类型族下使用的变量”与“根本不使用变量”一样。

您可以通过向eTable 添加一个Proxy 参数来解决这个问题，这样就可以修复类型检查器可以“向后运行”的类型变量e。所以eTable :: Proxy e -> Table (Relation e)。

或者，使用TypeApplications 扩展名，您现在可以按照错误消息的建议进行操作并打开AllowAmbiguousTypes 以使课程被接受，然后使用eTable @(Int, Bool) 之类的东西来告诉编译器你想要e的选择。这在类型注释eTable :: Table (Relation (Int, Bool)) 不起作用的情况下起作用的原因是类型注释是在类型检查器自上而下查看时添加到上下文的额外信息，但类型应用程序在类型检查器查看时添加额外信息底部-向上。而不是“这个表达式必须有一个与这个类型统一的类型”，而是“这个多态函数是在这个类型上实例化的”。

---

¹ 类型构造函数实际上比注入性更受限制；将Test 应用于任何类型a 会产生具有已知结构Test a 的类型，因此Haskell 类型的整个宇宙都直接反映在Test t 形式的类型中。一个更通用的单射类型函数可以做更多的“重新排列”，例如将Int 映射到Bool，只要它没有同时将Bool 映射到Bool。

²由组合表达式的子部分产生的类型

³ 来自使用它的上下文所需的类型