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

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

请注意，重叠的实例不会解析，尽管为此提供了杂注 结束。

 

一个解决方案。

经过一些猜测才得出以下调整后的定义：

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. 为什么在第一个代码段中没有解决重叠？
2. 为什么在第二个代码段中解决了重叠？

但是，如果这些问题相互关联，也许一个单一的、统一的理论将有助于更好地解释这种情况。

 

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

 

---

注意我 用ghc8.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 #-}编译指示没有任何作用(至少与问题有关(。因此，在解析约束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，第二个实例应该没有编译指示。这样，所有将来的实例都隐式地重叠 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)

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

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

另请参阅全康手册。