0 
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module OverlappingSpecificsError where

class EqM a b where
    (===) :: a -> b -> Bool

instance {-# OVERLAPPABLE #-} Eq a => EqM a a where
    a === b = a == b

instance {-# OVERLAPPABLE #-} EqM a b where
    a === b = False

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

aretheyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyeq (Left a1) (Right b2) = a1 === b2

既不编译aretheyreallyeq也不aretheyeq编译，但是 for 的错误对aretheyreallyeq我来说是有意义的，并且还告诉我不aretheyeq应该给出错误：GHCi 建议的可能 for EqMin的实例之一aretheyeq应该是不可能的，因为aretheyreallyeq. 这是怎么回事？

关键是，GHCi 坚持认为 的两个实例EqM都适用于aretheyeq. But a1is of typea和b2is of type b，所以为了使第一个实例适用，它必须具有类型a和b统一。

但这应该是不可能的，因为它们在函数签名处被声明为类型变量（也就是说，使用第一个EqM实例会导致函数为 type Either a a -> Either a a -> Bool，并且aretheyreallyeq告诉我 GHCi 不允许这样做（无论如何都是我所期望的）。

我是否遗漏了什么，或者这是如何检查具有多参数类型类的重叠实例的错误？

我在想这可能与这样一个事实有关，a并且b以后可以进一步实例化到它们相等的点， outside aretheyeq，然后第一个实例是有效的？但对于aretheyreallyeq. 唯一的区别是，如果他们不统一，我们可以选择aretheyeq，但我们没有aretheyreallyeq。在任何情况下，Haskell 没有动态调度有很多好的和明显的原因，所以有什么害怕提交实例总是有效的，无论以后a是否b统一也许有某种方法可以在以某种方式调用函数时选择实例？

值得注意的是，如果我删除第二个实例，那么该函数显然仍然无法编译，说明找不到实例EqM a b。因此，如果我没有那个实例，那么没有一个有效，但是当那个有效时，突然另一个也有效并且我有重叠？几英里外的我闻起来像虫子。

4

4 回答 4

3

泛型变量上的实例匹配以这种方式工作，以防止一些潜在的混乱（和危险）场景。

如果编译器屈服于您的直觉并EqM a b在编译时选择了实例aretheyeq（因为a并不b一定要统一，正如您所说），那么以下调用：

x = aretheyeq (Left 'z') (Right 'z')

会返回False，与直觉相反。

问：等一下！但是在这种情况下，a ~ Char和b ~ Char，我们也有Eq a和Eq b，这意味着Eq Char，应该可以选择EqM a a实例，不是吗？

嗯，是的，我想这在理论上可能会发生，但 Haskell 就是不能这样工作。类实例只是传递给函数的额外参数（作为方法字典），因此为了存在实例，它必须在函数本身内明确地选择，或者必须从使用者传入。

前者（明确选择的实例）必然要求只有一个实例。实际上，如果您删除EqM a a实例，您的函数将编译并始终返回False.

后者（从消费者传递一个实例）意味着对函数的约束，如下所示：

aretheyeq :: EqM a b => Either a b -> Either a b -> Bool

您要问的是 Haskell 本质上具有此功能的两个不同版本：一个需要该功能a ~ b并选择EqM a a实例，另一个不需要该功能并选择EqM a b实例。

然后编译器会巧妙地选择“正确”的版本。所以如果我打电话aretheyeq (Left 'z') (Right 'z')，第一个版本会被调用，但如果我打电话aretheyeq (Left 'z') (Right 42)- 第二个。

但现在再想一想：如果有两个版本aretheyeq，选择哪一个取决于类型是否相等，那么考虑一下：

dummy :: a -> b -> Bool
dummy a b = aretheyeq (Left a) (Right b)

如何dummy知道aretheyeq选择哪个版本？所以现在也必须有两个版本dummy：一个用于何时a ~ b，另一个用于其他情况。

等等。涟漪效应一直持续到出现具体类型为止。

问：等一下！为什么有两个版本？不能只有一个版本，然后根据传入的参数决定做什么？

啊，但它不能！这是因为类型在编译时被擦除。当函数开始运行时，它已经编译好了，没有更多的类型信息。所以一切都必须在编译时决定：选择哪个实例，以及从中产生的连锁反应。

于 2020-02-13T03:41:25.713 回答
2

从完全按照记录的方式工作的意义上来说，这不是一个错误。从...开始

现在假设，在某个客户端模块中，我们正在搜索目标约束的一个实例(C ty1 .. tyn)。搜索工作如下：

寻找候选实例的第一阶段按您的预期工作；EqM a b是唯一的候选人，因此是主要候选人。但最后一步是

现在找到与目标约束统一但不匹配的所有实例或范围内给定约束。当目标约束被进一步实例化时，此类非候选实例可能匹配。如果它们都是不连贯的顶级实例，则搜索成功，返回主要候选者。否则搜索失败。

该EqM a a实例属于此类，并且不是不连贯的，因此搜索失败。您可以通过将其标记为{-# INCOHERENT #-}而不是可重叠来实现您想要的行为。

于 2020-02-13T08:09:44.757 回答
0

为了进一步完成 Alexey 的回答，这确实给了我应该做些什么来实现我想要的行为的提示，我编译了以下稍微不同的情况的最小工作示例，更类似于我的实际用例（与 相关ExistentialQuantification）：

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
module ExistentialTest where

class Class1 a b where
    foo :: a -> b

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either b a) where
    foo x = Right (x <> x)

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either a b) where
    foo x = Left x

data Bar a = Dir a | forall b. Class1 b a => FromB b

getA :: Bar a -> a
getA (Dir a) = a
getA (FromB b) = foo b

createBar :: Bar (Either String t)
createBar = FromB "abc"

createBar2 :: Bar (Either t String)
createBar2 = FromB "def"

如果您删除注释，您会得到与我在and{-# INCOHERENT #-}上的原始示例完全相同的编译错误，并且要点是相同的：很明显，唯一合适的实例是第二个，而唯一合适的实例是第一个，但是 Haskell 拒绝编译，因为它在使用它时可能会造成明显的混乱，直到你用.createBarcreateBar2createBarcreateBar2 INCOHERENT

然后，代码完全按照您的预期工作：getA createBar返回Left "abc"而getA createBar2返回Right "defdef"，这正是合理类型系统中唯一可能发生的事情。

因此，我的结论是：INCOHERENT注释正是为了允许我从一开始就想做的事情，而 Haskell 不会抱怨可能令人困惑的实例，并且确实采用了唯一有意义的实例。对于是否INCOHERENT可以使用任意一个（这显然是坏和危险的）编译，即使在考虑到所有内容后确实仍然重叠的实例仍然存在疑问。因此，我的结论的一个推论是：仅INCOHERENT在您绝对需要并且绝对相信确实只有一个有效实例时才使用。

我仍然认为 Haskell 没有更自然和安全的方法来告诉编译器停止担心我可能会感到困惑并做显然是解决问题的唯一类型检查答案的事情有点荒谬......

于 2020-02-16T03:22:07.927 回答
-1

aretheyreallyeq失败是因为作用域中有两个不同的类型变量。在

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

a1 :: a, 和b2 :: b, 没有方法可以比较可能不同类型的值（因为这是它们的声明方式），所以这失败了。当然，这与任何启用的扩展或 pragma 无关。

aretheyeq失败是因为有两个实例可以匹配，而不是它们肯定匹配。我不确定您使用的是什么版本的 GHC，但这是我看到的异常消息，对我来说似乎很清楚：

    • Overlapping instances for EqM a b arising from a use of ‘===’
      Matching instances:
        instance [overlappable] EqM a b -- Defined at /home/tmp.hs:12:31
        instance [overlappable] Eq a => EqM a a
          -- Defined at /home/tmp.hs:9:31
      (The choice depends on the instantiation of ‘a, b’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: a1 === b2
      In an equation for ‘aretheyeq’:
          aretheyeq (Left a1) (Right b2) = a1 === b2

在这种情况下，我的解释是，给定 a 和 b 的某些选择，可能存在多个不同的匹配实例。

于 2020-02-13T02:59:43.383 回答