Haskell：实例中的等式约束 [英] Haskell: Equality constraint in instance

问题描述

我正在阅读 ClassyPrelude 的公告并到达此处：

  instance（b〜c，CanFilterFunc ba）=> CanFilter（b  - > c）a其中
 filter = filterFunc 
  

这可能不起作用：

  instance（CanFilterFunc ba）=> CanFilter（c  - > c）a其中
 filter = filterFunc 
  

我，因为 c 与左边的约束完全无关。 然而，文章和我不明白的是为什么这是行不通的：

  instance（CanFilterFunc ba）=> CanFilter（b  - > b）a where 
 filter = filterFunc 
  

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

解决方案

迈克尔已经在他的博客文章中给出了一个很好的解释，但是我我们将尝试用一个（人为的，但相对较小的）例子来说明它。

我们需要以下扩展：

  { - ＃LANGUAGE FlexibleInstances，TypeFamilies＃ - } 
  

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

  class Twice1 f where 
 twice1 :: f  - > f 
 
 class Twice2 f where 
 twice2 :: f  - > f 
  

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

  instance Twice1（a  - > a）其中
 twice1 f = f。 f 
 
实例（a〜b）=>两次2（a  - > b）其中
两次f = f。 f 
  

为了显示差异，让我们定义另一个重载函数，如下所示：

  class示例a其中
 transform :: Int  - > a 
 
实例示例Int其中
变换n = n + 1 
 
实例示例Char其中
变换_ ='x'
  

现在我们处于一个可以看到差异的点。一旦我们定义

  apply1 x = twice1变换x 
 apply2 x =两次2变换x 
  

并向GHC请求推断的类型，我们得到那个

  apply1 ::（Example a，Twice1（Int  - > a））=> Int  - > 
 apply2 :: Int  - > Int 
  

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

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

所以这是关于GHC实例解析的一个相当微妙的点，并且这里的等式约束有助于GHC的类型检查器，这需要用户减少类型注释。

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

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

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

解决方案

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

We need the following extensions:

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}

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

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

and ask GHC for the inferred types, we get that

apply1 :: (Example a, Twice1 (Int -> a)) => Int -> a
apply2 :: Int -> 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.

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.

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屋！