haskell - IncoherentInstances 如何工作？

Question

玩弄 some code :

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Arity f where
  arity :: f -> Int

instance Arity x where
  arity _ = 0

instance Arity f => Arity ((->) a f) where
  arity f = 1 + arity (f undefined)

没有IncoherentInstances:

ghci> arity foldr
blah blah ambiguous blah blah possible fix blah
ghci> arity (foldr :: (a -> Int -> Int) -> Int -> [a] -> Int)
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3
2

如果我们将 IncoherentInstances 添加到编译指示列表中，那么它可以处理 foldr 而无需单态类型签名，但它在 lambda 上得到错误的答案:

ghci> arity foldr
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3 -- should be 2
0

不连贯实例背后的黑魔法是什么？为什么它会这样做？

Answer 1

嗯，这相当复杂。让我们从不明确的错误开始:

<interactive>:1:1:
    Ambiguous type variable `b0' in the constraint:
      (Arity b0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity foldr
    In an equation for `it': it = arity foldr

通常，在没有重叠实例的情况下，当尝试将类型与类进行匹配时，它将将该类型与该类的所有实例进行比较。如果恰好有一个匹配项，它将使用该实例。否则，您将收到无实例错误(例如使用 show (*))，或重叠实例错误。例如，如果您从上述程序中删除 OverlappingInstances 语言功能，您将收到以下错误:arity (&&):

<interactive>:1:1:
    Overlapping instances for Arity (Bool -> Bool -> Bool)
      arising from a use of `arity'
    Matching instances:
      instance Arity f => Arity (a -> f)
        -- Defined at tmp/test.hs:9:10-36
      instance Arity x -- Defined at tmp/test.hs:12:10-16
    In the expression: arity (&&)
    In an equation for `it': it = arity (&&)

它匹配Arity (a -> f)，因为a可以是Bool，f可以是 bool -> bool 。它还匹配 Arity x，因为 x 可以是 Bool -> Bool -> Bool。

使用OverlappingInstances，当遇到两个或多个实例可以匹配的情况时，如果有一个最具体的实例，就会选择它。如果X可以匹配Y，则实例X比实例Y更具体，但反之则不然。

在本例中，(a -> f) 与 x 匹配，但 x 与 (a -> f) 不匹配)(例如，考虑x为Int)。因此 Arity (a -> f) 比 Arity x 更具体，因此如果两者都匹配，则选择前者。

使用这些规则，arity (&&) 将首先匹配 Arity ((->) a f)，其中 a 为 Bool，f 为 Bool -> Bool。下一场比赛的 a 将为 Bool，f 为 bool。最后它将结束匹配Arity x，其中x为Bool。

<小时/>

请注意，上述函数的(&&)结果是具体类型Bool。但是，当类型不具体时会发生什么？例如，让我们看一下 arity undefined 的结果。 undefined 的类型为 a，因此它不是具体类型:

<interactive>:1:1:
    Ambiguous type variable `f0' in the constraint:
      (Arity f0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity undefined
    In an equation for `it': it = arity undefined

您会得到一个不明确的类型变量错误，就像foldr 的错误一样。为什么会出现这种情况？这是因为根据 a 是什么，将需要不同的实例。如果 a 为 Int，则应匹配 Arity x 实例。如果 a 是 Int -> Int，则应匹配 Arity ((->) a f) 实例。因此，ghc 拒绝编译该程序。

如果您记下foldr 的类型:foldr::forall a b。 (a -> b -> b) -> b -> [a] -> b，你会注意到同样的问题:结果不是一个具体的变量。

<小时/>

这就是 IncoherentInstances 的用武之地:启用该语言功能后，它将忽略上述问题，而只选择一个始终与变量匹配的实例。例如，对于arity undefined，Arity x将始终匹配a，因此结果将为0。对于也做了类似的事情文件夹。

<小时/>

现在来说第二个问题，为什么启用 IncoherentInstaces 时 arity $\x y -> 3 返回 0？

这是非常奇怪的行为。下面的 ghci session 将显示它有多么奇怪:

*Main> let f a b = 3
*Main> arity f
2
*Main> arity (\a b -> 3)
0

这让我认为 ghc 中存在一个错误，其中 \a b -> 3 被 IncoherentInstances 视为具有类型 x 而不是 a -> b -> Int。我想不出这两个表达式不应该完全相同的任何原因。