haskell - 我如何读取这个孔错误

Question

我正在尝试编写 flatMap 的实现。但这无关紧要，我真的很想理解错误消息。但就目前而言，我有:

flatMap ::
(a -> List b)
  -> List a
  -> List b
flatMap f xs = foldRight undefined undefined _undefined

这会导致类型孔出现以下错误:

Found hole ‘_undefined’ with type: List a0
    Where: ‘a0’ is an ambiguous type variable
    Relevant bindings include
      xs :: List a (bound at src/Course/List.hs:266:11)
      f :: a -> List b (bound at src/Course/List.hs:266:9)
      flatMap :: (a -> List b) -> List a -> List b
        (bound at src/Course/List.hs:266:1)
    In the third argument of ‘foldRight’, namely ‘_undefined’
    In the expression: foldRight undefined undefined _undefined
    In an equation for ‘flatMap’:
        flatMap f xs = foldRight undefined undefined _undefined

我知道这个洞的正确钉子是 xs，但我不明白为什么 haskell 编译器给它一个表示为 List a0 的类型，以及它与我要使用的 List a 类型有何关系？

我认为这与整体可以采用 List a 类型的超集或其他东西有关？那么为什么不直接将其称为 List b 而不是专门称为 List a0。

干杯，吉姆

Answer 1

粗略地说，编译器推断类型如下。

让我们为每个未定义赋予一个不同的类型unknown:

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a1) (undefined :: b1) (_undefined :: c1)

现在，foldRight 需要一个具有类似 a2 -> b2 -> b2 类型的二元函数，因此让我们使 a1 更精确。

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b1) (_undefined :: c1)

现在，foldRight 要求第二个 undefined 具有类型 b1 ~ b2，而最后一个必须具有类型 c1 ~列出a2。

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b2) (_undefined :: List a2)

(假设我们有 Nil 和 Cons 作为 List 类型的构造函数)

foldRight 的结果是 b2，但类型签名表明这实际上是 List b。因此，

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> List b -> List b) (undefined :: List b)
             (_undefined :: List a2)

现在我们完成了。请注意，没有任何约束可以让我们推断出 a2 ~ a，因此 a2 仍然是未知的，编译器无法为其建议更精确的类型，并且您的漏洞会生成您发布的 GHC 消息。

更具体地说，看看这个特化，其中a2 ~ Int:

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (g :: Int -> List b -> List b) (Nil :: List b) (Cons 3 Nil :: List Int)
   where g :: Int -> List b -> List b
         g y ys = ys

即使我们选择a2 ~ Int而不是a2 ~ a，上述类型检查也是如此。因此，编译器无法推断 a2 ~ a，因为未知类型 a2 有更多解决方案。