重叠多参数实例和实例特异性

Overlapping multi-parameter instances and instance specificity

{-# 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

aretheyreallyeqaretheyeq 都无法编译,但是 aretheyreallyeq 的错误对我来说很有意义,并且还告诉我 aretheyeq 不应该给出错误:一个由于 aretheyreallyeq 上的相同错误,GHCi 建议的 aretheyeq 中的 EqM 可能的实例应该是不可能的。怎么回事?

重点是,GHCi 坚持 EqM 的两个实例都适用于 aretheyeq。但是 a1a 类型而 b2b 类型,所以为了使第一个实例适用,它必须具有类型 ab统一。

但这应该是不可能的,因为它们在函数签名中被声明为类型变量(也就是说,使用第一个 EqM 实例会导致函数类型为 Either a a -> Either a a -> Bool ,并且 aretheyreallyeq 中的错误告诉我 GHCi 不允许这样做(这正是我所期望的)。

我是不是遗漏了什么,或者这是检查多参数类型 类 的重叠实例的错误?

我想这可能与以下事实有关 ab 稍后可以进一步实例化到它们在 aretheyeq 之外相等的程度,并且那么第一个实例 有效吗?但是aretheyreallyeq也是一样。唯一的区别是,如果它们永远不会统一,我们可以选择 aretheyeq,但我们不会选择 aretheyreallyeq。在任何情况下,Haskell 都没有动态调度,原因有很多,而且很明显,所以提交实例 总是 工作的恐惧是什么,无论以后是否ab 是统一的吗?也许有一些方法可以让调用函数时选择实例成为可能?

值得注意的是,如果我删除了第二个实例,那么该函数显然仍然无法编译,说明找不到实例EqM a b。因此,如果我没有那个实例,那么 none 会起作用,但是当那个实例起作用时,突然另一个也起作用并且我有重叠?千里之外我闻起来像臭虫。

aretheyreallyeq 失败,因为范围内有两个不同类型的变量。在

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

a1 :: ab2 :: b,没有方法可以比较可能不同类型的值(因为它们是这样声明的),所以失败了。当然,这与任何启用的扩展或编译指示无关。

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 的特定选择,可能存在多个不同的匹配实例。

通用变量的实例匹配以这种方式工作,以防止出现一些可能令人困惑(和危险)的情况。

如果编译器屈服于你的直觉并在编译 aretheyeq 时选择了 EqM a b 实例(因为 ab 不一定统一,因为你'再说),则调用如下:

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

会returnFalse,与直觉相反。

Q: 稍等!但是在这种情况下,a ~ Charb ~ Char,我们还有Eq aEq b,这意味着Eq Char,应该可以选择EqM a a 实例,不是吗?

嗯,是的,我想这 可以 在理论上发生,但 Haskell 只是行不通。 Class 实例只是传递给函数的额外参数(作为方法字典),因此为了有一个实例,它必须在函数本身内明确选择, 必须从消费者传入。

前者(可明确选择的实例)必然要求只有一个实例。事实上,如果您删除 EqM a a 实例,您的函数将编译并始终 returns False.

后者(从消费者传递一个实例)意味着对函数的约束,像这样:

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

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

然后编译器会巧妙地选择 "right" 版本。因此,如果我调用 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 时,另一个用于其他情况。

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

Q: 稍等!为什么有两个版本?不能只有一个版本,然后根据传入的参数决定做什么吗?

啊,但不能!这是因为类型在编译时被擦除。当函数开始到 运行 时,它已经被编译,并且没有更多的类型信息。所以一切都必须在编译时决定:选择哪个实例,以及它的连锁反应。

这不是工作意义上的错误 exactly as documented。从

开始

Now suppose that, in some client module, we are searching for an instance of the target constraint (C ty1 .. tyn). The search works like this:

寻找候选实例的第一阶段如您所料; EqM a b 是唯一的候选人,因此是主要候选人。但最后一步是

Now find all instances, or in-scope given constraints, that unify with the target constraint, but do not match it. Such non-candidate instances might match when the target constraint is further instantiated. If all of them are incoherent top-level instances, the search succeeds, returning the prime candidate. Otherwise the search fails.

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

为了进一步完成 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"

如果删除 {-# INCOHERENT #-} 注释,在 createBarcreateBar2 上会得到与我原来示例中完全相同的编译错误,重点是相同的:在createBar 很明显,唯一合适的实例是第二个,而在 createBar2 中,唯一合适的是第一个,但是 Haskell 拒绝编译,因为这种明显的混淆可能使用它时创建,直到你用 INCOHERENT.

注释它们

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

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

我仍然认为 Haskell 没有更自然和安全的方式告诉编译器停止担心我可能被混淆并做显然是唯一类型检查答案的事情有点荒谬问题...