Haskell:例如等式约束 [英] Haskell: Equality constraint in instance

问题描述

我正在阅读 ClassyPrelude 的公告，然后来到这里:

I was reading through the announcement of ClassyPrelude and got to here:

instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a where
    filter = filterFunc

作者随后提到这行不通:

The writer then mentioned that this would not work:

instance (CanFilterFunc b a) => CanFilter (c -> c) a where
    filter = filterFunc

这对我来说很有意义，因为 c 与左侧的约束完全无关.

Which makes sense to me, as c is completely unrelated to the constraint on the left.

然而，文章中没有提到的，我不明白的是为什么这行不通:

However, what isn't mentioned in the article and what I don't understand is why this wouldn't work:

instance (CanFilterFunc b a) => CanFilter (b -> b) a where
    filter = filterFunc

有人可以解释为什么这与第一个提到的定义不同吗?也许 GHC 类型推断的有效示例会有所帮助?

Could someone explain why this is different to the first mentioned definition? Perhaps a worked example of GHC type inference would be helpful?

推荐答案

Michael 在他的博客文章中已经给出了很好的解释，但我将尝试用一个(人为的，但相对较小的)示例来说明.

Michael already gives a good explanation in his blog article, but I'll try to illustrate it with a (contrived, but relatively small) example.

我们需要以下扩展:

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}

让我们定义一个比 CanFilter 更简单的类，只有一个参数.我定义了类的两个副本，因为我想演示两个实例之间的行为差​​异:

Let's define a class that is simpler than CanFilter, with just one parameter. I'm defining two copies of the class, because I want to demonstrate the difference in behaviour between the two instances:

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

现在，让我们为每个类定义一个实例.对于Twice1，我们直接将类型变量固定为相同，对于Twice2，我们允许它们不同，但添加了等式约束.

Now, let's define an instance for each class. For Twice1, we fix the type variables to be the same directly, and for Twice2, we allow them to be different, but add an equality constraint.

instance Twice1 (a -> a) where
  twice1 f = f . f

instance (a ~ b) => Twice2 (a -> b) where
  twice2 f = f . f

为了显示差异，让我们定义另一个像这样的重载函数:

In order to show the difference, let us define another overloaded function like this:

class Example a where
  transform :: Int -> a

instance Example Int where
  transform n = n + 1

instance Example Char where
  transform _ = 'x'

现在我们可以看到差异了.一旦我们定义

Now we are at a point where we can see a difference. Once we define

apply1 x = twice1 transform x
apply2 x = twice2 transform x

向 GHC 询问推断的类型，我们得到

and ask GHC for the inferred types, we get that

apply1 :: (Example a, Twice1 (Int -> a)) => Int -> a
apply2 :: Int -> Int

这是为什么?好吧，Twice1 的实例仅在函数的源类型和目标类型相同时才会触发.对于 transform 和给定的上下文，我们不知道.GHC 只会在右侧匹配时应用一个实例，因此我们留下了未解析的上下文.如果我们尝试说apply1 0，将会出现一个类型错误，指出仍然没有足够的信息来解决重载.在这种情况下，我们必须明确指定结果类型为 Int 才能通过.

Why is that? Well, the instance for Twice1 only fires when source and target type of the function are the same. For transform and the given context, we don't know that. GHC will only apply an instance once the right hand side matches, so we are left with the unresolved context. If we try to say apply1 0, there will be a type error saying that there is still not enough information to resolve the overloading. We have to explicitly specify the result type to be Int in this case to get through.

然而，在Twice2 中，实例适用于任何函数类型.GHC 会立即解决它(GHC 永远不会回溯，所以如果一个实例明确匹配，它总是被选中)，然后尝试建立先决条件:在这种情况下，等式约束，然后强制结果类型为 Int 并允许我们解决 Example 约束.我们可以说 apply2 0 没有进一步的类型注释.

However, in Twice2, the instance is for any function type. GHC will immediately resolve it (GHC never backtracks, so if an instance clearly matches, it's always chosen), and then try to establish the preconditions: in this case, the equality constraint, which then forces the result type to be Int and allows us to resolve the Example constraint, too. We can say apply2 0 without further type annotations.

所以这是关于 GHC 实例解析的一个相当微妙的点，这里的等式约束以一种需要用户更少类型注释的方式帮助 GHC 的类型检查器.

So this is a rather subtle point about GHC's instance resolution, and the equality constraint here helps GHC's type checker along in a way that requires fewer type annotations by the user.

这篇关于Haskell:例如等式约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！