`~`(代字号)在实例上下文中意味着什么,为什么在某些情况下需要解决重叠？

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. 为什么在第二个片段中解决了重叠？

但是,如果问题是相关的,也许一个统一的理论可以更好地解释这个案例.

 

PS关于关闭/重复投票   我知道这~意味着类型相等,我有意识地使用它来获得我需要的行为(特别是,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 #-}编译指示不执行任何操作（至少与问题相关）。因此，在解析约束时D [Integer] [Integer]，编译器发现两个实例都是候选实例，两者都不比另一个更具体，并给出错误。

在

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

第二个实例比第一个实例更具体，因为可以实例化第一个实例u := u; a := f x以获取第二个实例。现在，pragma 发挥了作用。解析 时D [Integer] [Integer]，两个实例都匹配，第一个实例匹配u := [Integer]; a := [Integer]，第二个实例匹配u := [Integer]; f := []; x := Integer。然而，第二个更具体并且OVERLAPPING，因此第一个实例被丢弃作为候选并使用第二个实例。（旁注：我认为第一个实例应该是OVERLAPPABLE，第二个实例应该没有编译指示。这样，所有未来的实例都隐式地与包罗万象的实例重叠，而不必对每个实例进行注释。）

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

可视化正在发生的情况的一种方法是维恩图。从第一次尝试开始，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 手册。