为什么在 Haskell 中选择类型类实例时不考虑上下文？

Question

我明白，当有

instance (Foo a) => Bar a
instance (Xyy a) => Bar a

GHC 不考虑上下文，实例被报告为重复。

什么是违反直觉的，（我猜）在选择一个实例之后，它仍然需要检查上下文是否匹配，如果不匹配，则丢弃该实例。那么为什么不颠倒顺序，丢弃上下文不匹配的实例，然后继续处理剩余的集合。

这会以某种方式难以处理吗？我看到它会如何提前导致更多的约束解析工作，但是就像有 UndecidableInstances / IncoherentInstances 一样，当“我知道我在做什么”时，难道不能有 ConsiderInstanceContexts 吗？

Answer 1

这打破了开放世界的假设。假设：

class B1 a
class B2 a
class T a

如果我们允许约束来消除实例的歧义，我们可以写

instance B1 a => T a
instance B2 a => T a

可以写

instance B1 Int

现在，如果我有

f :: T a => a

然后f :: Int 工作。但是，开放世界假设表明，一旦某些东西起作用，添加更多实例就不会破坏它。我们的新系统不服从：

instance B2 Int

会使f :: Int 模棱两可。应该使用T 的哪个实现？

另一种说法是你破坏了连贯性。类型类保持一致意味着只有一种方法可以满足给定的约束。在普通的 Haskell 中，约束 c 只有一个实现。即使有重叠的实例，连贯性通常也适用。这个想法是instance T a 和instance {-# OVERLAPPING #-} T Int 不会破坏连贯性，因为不能欺骗 GHC 在后者可以使用的地方使用前一个实例。 （你可以用孤儿来欺骗它，但你不应该。）至少对我来说，连贯性似乎有点可取。在某种意义上，类型类的使用是“隐藏的”，强制它是明确的是有意义的。你也可以用IncoherentInstances 和/或unsafeCoerce 打破连贯性，但是，你知道的。

在类别理论方面，类别Constraint 细：从一个Constraint 到另一个最多有一个instance/arrow。我们首先构造两个箭头a : () => B1 Int 和b : () => B2 Int，然后我们通过添加新箭头x_Int : B1 Int => T Int、y_Int : B2 Int => T Int 来打破薄度，这样x_Int . a 和y_Int . b 都是箭头() => T Int，它们并不相同。钻石问题，有人吗？

Answer 2

这并没有回答您为什么会这样的问题。但是请注意，您始终可以定义一个新类型包装器来消除两个实例之间的歧义：

newtype FooWrapper a = FooWrapper a
newtype XyyWrapper a = XyyWrapper a

instance (Foo a) => Bar (FooWrapper a)
instance (Xyy a) => Bar (XyyWrapper a)

这还有一个额外的好处，即通过传递 FooWrapper 或 XyyWrapper ，您可以明确控制如果您的 a 恰好满足两者，您想使用两个实例中的哪一个。

Answer 3

类有点奇怪。最初的想法（仍然非常有效）是一种围绕 data 语句的语法糖。例如你可以想象：

data Num a = Num {plus :: a -> a -> a, ... , fromInt :: Integer -> a}
numInteger :: Num Integer
numInteger = Num (+) ... id

然后您可以编写具有例如的函数类型：

test :: Num x -> x -> x -> x -> x
test lib a b c = a + b * (abs (c + b))
    where (+) = plus lib
          (*) = times lib
          abs = absoluteValue lib

所以想法是“我们将自动派生所有这些库代码”。问题是，我们如何找到我们想要的库？如果我们有一个Num Int 类型的库，这很容易，但是我们如何将它扩展到基于类型函数的“约束实例”：

fooLib :: Foo x -> Bar x
xyyLib :: Xyy x -> Bar x

Haskell 中的当前解决方案 是对这些函数的输出类型进行类型模式匹配，并将输入传播到结果声明。但是当有两个相同类型的输出时，我们需要一个组合器将它们合并为：

eitherLib :: Either (Foo x) (Xyy x) -> Bar x

基本上问题是现在没有这种好的约束组合器。那是你的反对意见。

嗯，没错，但在实践中，有一些方法可以实现道德上相似的目标。假设我们用类型定义了一些函数：

data F
data X
foobar'lib :: Foo x -> Bar' x F
xyybar'lib :: Xyy x -> Bar' x X
bar'barlib :: Bar' x y -> Bar x

显然，y 是一种贯穿所有这些的“幻像类型”，但它仍然很强大，因为鉴于我们想要一个 Bar x，我们将传播对 Bar' x y 的需求，并考虑到对Bar' x y 我们将生成Bar' x X 或Bar' x y。所以通过幻像类型和多参数类型类，我们得到了我们想要的结果。

更多信息：https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap

Answer 4

添加回溯会使实例解析需要指数级的时间，在最坏的情况下。

从本质上讲，实例变成了形式的逻辑语句

P(x) => R(f(x)) /\ Q(x) => R(f(x))

相当于

(P(x) \/ Q(x)) => R(f(x))

在计算上，这个检查的成本是（在最坏的情况下）

c_R(n) = c_P(n-1) + c_Q(n-1)

假设 P 和 Q 的成本相似

c_R(n) = 2 * c_PQ(n-1)

这会导致指数级增长。

为了避免这个问题，重要的是要有快速的方法来选择一个分支，即有形式的子句

((fastP(x) /\ P(x)) \/ (fastQ(x) /\ Q(x))) => R(f(x))

其中fastP和fastQ在常数时间内是可计算的，并且不兼容，因此最多需要访问一个分支。

Haskell 认为这种“快速检查”是头部兼容性（因此忽略上下文）。当然，它可以使用其他快速检查——这是一个设计决定。