为什么在 Haskell 中选择类型类实例时不考虑上下文? [英] Why context is not considered when selecting typeclass instance in Haskell?

问题描述

我明白当有

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

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

GHC doesn't consider the contexts, and the instances are reported as duplicate.

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

What is counterintuitive, that (I guess) after selecting an instance, it still needs to check if the context matches, and if not, discard the instance. So why not reverse the order, and discard instances with non-matching contexts, and proceed with the remaining set.

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

Would this be intractable in some way? I see how it could cause more constraint resolution work upfront, but just as there is UndecidableInstances / IncoherentInstances, couldn't there be a ConsiderInstanceContexts when "I know what I am doing"?

推荐答案

这打破了开放世界的假设.假设:

This breaks the open-world assumption. Assume:

class B1 a
class B2 a
class T a

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

If we allow constraints to disambiguate instances, we may write

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

并且可以写

instance B1 Int

现在，如果我有

f :: T a => a

然后 f :: Int 起作用.但是，开放世界的假设表明，一旦某件事奏效，添加更多实例就无法破坏它.我们的新系统不服从:

Then f :: Int works. But, the open world assumption says that, once something works, adding more instances cannot break it. Our new system doesn't obey:

instance B2 Int

会使 f :: Int 不明确.应该使用 T 的哪个实现?

will make f :: Int ambiguous. Which implementation of T should be used?

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

Another way to state this is that you've broken coherence. For typeclasses to be coherent means that there is only one way to satisfy a given constraint. In normal Haskell, a constraint c has only one implementation. Even with overlapping instances, coherence generally holds true. The idea is that instance T a and instance {-# OVERLAPPING #-} T Int do not break coherence, because GHC can't be tricked into using the former instance in a place where the latter would do. (You can trick it with orphans, but you shouldn't.) Coherence, at least to me, seems somewhat desirable. Typeclass usage is "hidden", in some sense, and it makes sense to enforce that it be unambiguous. You can also break coherence with IncoherentInstances and/or unsafeCoerce, but, y'know.

以范畴论的方式，范畴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 不相同.钻石问题，有人吗?

In a category theoretic way, the category Constraint is thin: there is at most one instance/arrow from one Constraint to another. We first construct two arrows a : () => B1 Int and b : () => B2 Int, and then we break thinness by adding new arrows x_Int : B1 Int => T Int, y_Int : B2 Int => T Int such that x_Int . a and y_Int . b are both arrows () => T Int that are not identical. Diamond problem, anyone?

这篇关于为什么在 Haskell 中选择类型类实例时不考虑上下文?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！