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

Question

我有一个类型 class 定义如下：

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，反之亦然。

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

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

我不太确定 Table and 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 未在 class 中使用无关（您通过使用函数依赖性来阻止）。

错误信息的关键部分是：

  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 b^{1[ 不同的类型=144=]。这意味着当类型检查时你可以 "run them backwards";如果我有两种类型 t1 和 t2，它们都是应用 Test 的结果，并且我知道 t1 和 t2 应该是相等，那么我可以 "unapply" Test 获取参数类型并检查它们是否相等（或者推断其中一个是什么，如果它是我还没有弄清楚的，另一个是已知的, 等等).}

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

不幸的是，由于标准 Haskell 只有类型构造函数，Haskell 程序员受过良好训练，只能假设类型检查器可以通过复合类型向后工作以连接组件。我们经常甚至没有注意到类型检查器需要向后工作，我们已经习惯于只查看具有相似结构的类型表达式并在不检查所有内容的情况下跳到明显的结论类型检查器必须经过的步骤。但是因为类型检查是基于自下而上² 和自上而下³ 计算每个表达式的类型并确认它们是一致的, 其类型涉及类型族的类型检查表达式很容易运行陷入歧义问题，它看起来 "obviously" 对我们人类来说是明确的。

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

的 Table (Relation e)

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

即使每次使用 eTable（如 eTable :: Table (Relation (Int, Bool))）时添加类型注释也无济于事。类型注解只会向自上而下的视图添加额外的信息，而我们通常已经有了这些信息。类型检查器仍然存在一个问题，即 e 与 (Int, Bool) 的其他选择可能（无论是否确实存在）导致 eTable 匹配该类型注释，因此它不知道要使用哪个实例。任何可能使用eTable都会有这个问题，所以当你定义class时它会被报告为错误。这基本上与当您有一个 class 时遇到问题的原因相同，这些成员的类型不使用 class 头部中的所有类型变量；你必须考虑 "variable only used under a type family" 和 "variable isn't used at all".

你可以通过向 eTable 添加一个 Proxy 参数来解决这个问题，这样就可以修复类型检查器 可以 [=143] 的类型变量 e =] "run backwards"。所以 eTable :: Proxy e -> Table (Relation e).

或者，使用 TypeApplications 扩展，您现在可以按照错误消息的建议进行操作，并打开 AllowAmbiguousTypes 以获得 class接受，然后使用 eTable @(Int, Bool) 之类的东西告诉编译器您想要 e 的哪个选择。这在类型注释 eTable :: Table (Relation (Int, Bool)) 不起作用的情况下起作用的原因是类型注释是当类型检查器自上而下查看时添加到上下文的额外信息，但是当类型检查器是自下而上看。而不是 "this expression is required to have a type that unifies with this type" 它是 "this polymorphic function is instantiated at this type".

¹ 类型构造函数实际上比单射性更受限制；将 Test 应用于任何类型 a 会产生具有已知结构 Test a 的类型，因此 Haskell 类型的整个宇宙直接反映在 [=89= 形式的类型中].更通用的单射类型函数可以做更多的 "rearranging"，例如将 Int 映射到 Bool，只要它不也将 Bool 映射到 Bool .

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

³从使用的上下文需要的类型

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

Why does Haskell says this is ambiguous?

haskell

types

class

ambiguous