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

Question

并发症。

考虑以下 sn-p：

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."

 

我的问题。

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

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

1. 为什么在第一个 sn-p 中没有解决重叠？
2. 为什么在第二个 sn-p 中解决了重叠？

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

 

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

 

---

note 我用ghc8.4.3和8.6.0.20180810测试了上面的sn-ps

Answer 1

首先：在实例选择过程中只有实例头部很重要：=> 左边的内容无关紧要。因此，instance D a a 阻止选择，除非它们相等； instance ... => D u a 总是可以选择的。

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

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

两者都不比另一个更具体，因为没有将D a a 替换为D u (f x) 的替换a := ?，也没有将D u (f x) 替换为D a a 的任何替换u := ?; f := ?; x := x。 {-# 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，而第二个实例应该没有pragma。这样，所有未来的实例都会隐含地重叠catch-all实例，而不必注释每一个。）

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

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

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

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

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

另请参阅GHC manual。