单态约束对类型类约束的影响

Question

当添加baz 的类型声明时，此代码会中断：

baz (x:y:_) = x == y
baz [_] = baz []
baz [] = False

一个常见的解释（参见Why can't I declare the inferred type? 的例子）是因为多态递归。

但这种解释并不能解释为什么在另一个多态递归示例中效果会消失：

foo f (x:y:_) = f x y
foo f [_] = foo f []
foo f [] = False

它也没有解释为什么 GHC 认为没有类型声明的递归是单态的。

http://www.haskell.org/onlinereport/decls.html#sect4.5.5 中的reads 示例的解释可以应用于我的baz 案例吗？

即添加签名会消除单态性限制，如果没有限制，则会出现右侧 [] 的歧义，“固有歧义”类型为 forall a . Eq a => [a]?

Answer 1

baz 的方程在一个绑定组中，在输入整个组后进行泛化。如果没有类型签名，这意味着baz 被假定为具有单型，因此递归调用中[] 的类型由它给出（查看ghc 的-ddump-simpl 输出）。通过类型签名，编译器被明确告知该函数是多态的，因此它不能假定递归调用中[] 的类型相同，因此它是模棱两可的。

正如 John L 所说，在 foo 中，类型由 f 的出现固定 - 只要 f 具有单型。您可以通过将f 赋予与(==) 相同的类型来创建相同的歧义（这需要Rank2Types），

{-# LANGUAGE Rank2Types #-}
foo :: Eq b => (forall a. Eq a => a -> a -> Bool) -> [b] -> Bool
foo f (x:y:_) = f x y
foo f[_] = foo f []
foo _ [] = False

这给了

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `foo'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: foo f []
In an equation for `foo': foo f [_] = foo f []

Answer 2

您的第二个示例不是多态递归的。这是因为函数f 出现在递归定义的LHS 和RHS 上。还要考虑foo、(a -> a -> Bool) -> [a] -> Bool 的类型。这将列表元素类型修复为与f 的参数类型相同。因此，GHC 可以确定 RHS 上的空列表必须与输入列表具有相同的类型。

我不认为reads 的例子适用于baz 的情况，因为GHC 能够编译baz 而没有类型签名并且禁用了单态限制。因此，我希望 GHC 的类型算法有一些其他机制来消除歧义。