haskell - 什么是斯科勒姆？

Question

哎呀! GHCi 在我的代码中发现了 Skolems!

...
Couldn't match type `k0' with `b'
  because type variable `b' would escape its scope
This (rigid, skolem) type variable is bound by
  the type signature for
    groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a])
The following variables have types that mention k0
...

它们是什么？他们想要我的程序做什么？他们为什么要试图逃跑(忘恩负义的小捣蛋鬼)？

Answer 1

首先，上下文中的“刚性”类型变量意味着由该上下文之外的量词绑定(bind)的类型变量，因此不能与其他类型变量统一。

这与 lambda 绑定(bind)的变量非常相似:给定一个 lambda (\x -> ... )，从“外部”你可以将它应用到你喜欢的任何值，当然;但在内部，您不能简单地决定 x 的值应该是某个特定值。在 lambda 中为 x 选择一个值听起来很愚蠢，但这就是“无法匹配等等，刚性类型变量，等等”错误的含义。

请注意，即使不使用显式 forall 量词，任何顶级类型签名对于提到的每个类型变量都有一个隐式 forall。

当然，这不是您遇到的错误。 “转义类型变量”的含义更加愚蠢——就像有一个 lambda (\x -> ...) 并尝试使用 x 的特定值 <在 lambda 之外，独立于将其应用于参数。不，不是将 lambda 应用于某些内容并使用结果值 - 我的意思是实际上在定义的范围之外使用变量本身。

这种情况发生在类型上的原因(不像 lambda 的例子那样明显 absurd )是因为存在两个“类型变量”的概念:在统一期间，你有代表未确定类型的“变量”，这然后通过类型推断与其他此类变量进行识别。另一方面，您拥有上述量化类型变量，这些变量被明确标识为可能类型的范围。

考虑 lambda 表达式(\x -> x) 的类型。从完全不确定的类型 a 开始，我们看到它需要一个参数并将其缩小为 a -> b，然后我们看到它必须返回与它的参数，因此我们将其进一步缩小为 a -> a。但现在它适用于您可能想要的任何类型 a，因此我们给它一个量词 (forall a.a -> a)。

因此，当您有一个由量词绑定(bind)的类型时，GHC 推断应该与该量词范围之外的未确定类型统一，就会出现转义类型变量。

<小时/>

所以显然我忘记在这里实际解释术语“skolem 类型变量”，呵呵。正如评论中提到的，在我们的例子中，它本质上与“刚性类型变量”同义，所以上面仍然解释了这个想法。

我不太确定这个术语的起源，但我猜它涉及 Skolem normal form并用普遍性来表示存在量化，就像GHC中所做的那样。 skolem(或刚性)类型变量是一种在某些范围内由于某种原因具有未知但特定类型的变量 - 作为多态类型的一部分，来自存在数据类型，等等。