haskell - `~`(波浪号)在实例上下文中是什么意思，为什么在某些情况下需要解决重叠问题？

Question

一个并发症。

考虑以下代码段:

class                        D u a     where printD :: u -> a -> String
instance                     D a a     where printD _ _ = "Same type instance."
instance {-# overlapping #-} D u (f x) where printD _ _ = "Instance with a type constructor."

这就是它的工作原理:

λ printD 1 'a'
...
...No instance for (D Integer Char)...
...

λ printD 1 1
"Same type instance."

λ printD [1] [1]
...
...Overlapping instances for D [Integer] [Integer]
...

λ printD [1] ['a']
"Instance with a type constructor."

请注意，尽管提供了 pragma，但重叠实例并未解决
结尾。

一个解法。

需要一些猜测才能得出以下调整后的定义:

class                        D' u a     where printD' :: u -> a -> String
instance (u ~ a) =>          D' u a     where printD' _ _ = "Same type instance."
instance {-# overlapping #-} D' u (f x) where printD' _ _ = "Instance with a type constructor."

它按我预期的那样工作:

λ printD' 1 'a'
...
...No instance for (Num Char)...
...

λ printD' 1 1
"Same type instance."

λ printD' [1] [1]
"Instance with a type constructor."

λ printD' [1] ['a']
"Instance with a type constructor."

我的问题。

我很难理解这里发生了什么。有解释吗？

特别是，我可以提出两个单独的问题:

为什么在第一个片段中没有解决重叠？

为什么在第二个片段中解决了重叠？

但是，如果这些问题是相互关联的，也许一个单一的、统一的理论可以更好地解释这个案例。

附言关于关闭/重复投票我知道 ~表示类型相等，我有意识地使用它来获得我需要的行为(特别是 printD' 1 'a' 不匹配)。它几乎没有解释任何关于我提出的案例的具体内容，其中两种声明类型相等的方式( ~ 和 instance D a a)导致两种微妙不同的行为。



注意 我用 ghc 测试了上面的片段 8.4.3和 8.6.0.20180810

Answer 1

第一:在实例选择过程中只有实例头很重要:=> 左边是什么不要紧。所以，instance D a a除非它们相等，否则阻止选择； instance ... => D u a总是可以选择的。

现在，重叠编译指示只有在一个实例已经比另一个实例更“具体”时才会发挥作用。在这种情况下，“特定”意味着“如果存在可以将实例头 A 实例化为实例头 B 的类型变量的替换，则 B 比 A 更具体”。在

instance D a a
instance {-# OVERLAPPING #-} D u (f x)

两者都不比另一个更具体，因为没有替换 a := ?这使得 D a a进入 D u (f x) , 也没有任何替换 u := ?; f := ?; x := x这使得 D u (f x)进入 D a a . {-# OVERLAPPING #-} pragma 什么都不做(至少与问题有关)。所以，当解决约束 D [Integer] [Integer] ，编译器发现两个实例都是候选实例，两者都不比另一个更具体，并给出错误。

在

instance (u ~ a) => D u a
instance {-# OVERLAPPING #-} D u (f x)

第二个实例比第一个实例更具体，因为第一个实例可以用 u := u; a := f x 进行实例化到达第二个。编译指示现在发挥了作用。解析 D [Integer] [Integer] 时，两个实例匹配，第一个与 u := [Integer]; a := [Integer] ，第二个是 u := [Integer]; f := []; x := Integer .然而，第二个更具体， OVERLAPPING ，所以第一个被丢弃作为候选，第二个被使用。 (旁注:我认为第一个实例应该是 OVERLAPPABLE ，而第二个实例应该没有编译指示。这样，所有 future 的实例都会隐式地与 catch-all 实例重叠，而不必对每个实例进行注释。)

使用这个技巧，选择以正确的优先级完成，然后无论如何强制两个参数之间的相等性。显然，这种组合达到了您想要的效果。

可视化正在发生的事情的一种方法是维恩图。从第一次尝试开始， instance D a a和 instance D u (f x)形成两个集合，每个可以匹配的类型对的集合。这些集合确实重叠，但只有许多类型对 D a a匹配，并且只有许多对 D u (f x)火柴。两者都不能说更具体，所以 OVERLAPPING编译指示失败。在第二次尝试中， D u a实际上涵盖了类型对的整个宇宙，并且 D u (f x)是它的一个子集(阅读:内部)。现在， OVERLAPPING实用程序有效。以这种方式思考也向我们展示了另一种实现这项工作的方法，即创建一个完全覆盖第一次尝试的交集的新集合。

instance D a a
instance D u (f x)
instance {-# OVERLAPPING #-} (f x) (f x)

但是我会选择一个有两个实例的，除非你真的因为某种原因需要使用这个。

但是请注意，重叠的实例被认为有点脆弱。正如您所注意到的，通常很难理解选择了哪个实例以及为什么。人们需要考虑范围内的所有实例、它们的优先级，并且基本上在脑海中运行一种非平凡的选择算法以了解正在发生的事情。当跨多个模块(包括孤儿)定义实例时，事情变得更加复杂，因为选择规则可能会根据本地导入而有所不同。这甚至会导致不一致。最好尽可能避免它们。

另见 GHC manual .