为什么在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/箭头.我们首先构造两个箭头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屋！