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

Posted 2021-05-05

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

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类型的交易是什么导致的。

答案

模糊性的来源实际上与没有在类中使用的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中，构建复合类型表达式的唯一方法是使用类型构造函数，例如Test中的左侧data Test a = Test a。我可以将Test（善良的* -> *）应用到像Int（善良的*）这样的类型来获得类型Test Int（善良的*）。类型构造函数是injective，这意味着对于任何两种不同类型a和b，Test a是与Test b1不同的类型。这意味着在进行类型检查时，您可以“向后运行”;如果我有两种类型t1和t2，每个都是应用Test的结果，我知道t1和t2应该是相等的，那么我可以“取消应用”Test来获取参数类型并检查它们是否相等（或推断出其中一个是否是我尚未想到的，另一个是已知的，或等等）。

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

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

在你的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都会遇到这个问题，因此在定义类时会报告为错误。它基本上是出于同样的原因，当你有一个类有一些类型不使用类头中的所有类型变量的类时，你会遇到问题;你必须考虑“仅在类型族下使用的变量”与“根本不使用变量”相同。

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

或者，使用TypeApplications扩展，您现在可以执行错误消息建议并打开AllowAmbiguousTypes以接受类，然后使用eTable @(Int, Bool)之类的东西告诉编译器您想要的e选项。类型注释eTable :: Table (Relation (Int, Bool))不起作用的原因是类型注释是在类型检查器自上而下查看时添加到上下文的额外信息，但类型应用程序在类型检查器查看自下而上时添加额外信息。而不是“此表达式需要具有与此类型统一的类型”，而不是“此多态函数在此类型实例化”。

---

1类型构造函数实际上甚至比仅仅注入性更受限制;将Test应用于任何类型的a会产生一个具有已知结构Test a的类型，因此整个Haskell类型的世界在Test t形式的类型中直接镜像。更普遍的内射类型函数可以做更多的“重新排列”，例如将Int映射到Bool，只要它不将Bool映射到Bool。

2从通过组合表达式的子部分产生的类型

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

另一答案

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不是单射的。