什么是skolems？ [英] What are skolems?

问题描述

Eeek！ GHCi在我的代码中找到Skolems！

  ... 
无法将类型'k0'与'b' 
，因为类型变量`b'会跳过它的范围
这个（rigid，skolem）类型的变量受到
的限制
的类型签名groupBy :: Ord b => （a  - > b） - >设置 - >设置（b，[a]）
以下变量的类型提及k0 
 ... 
  

他们是什么？他们想要什么与我的程序？
为什么他们试图逃避（忘恩负义的小型blighters）？

解决方案

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

这很像一个lambda绑定的变量：给定一个lambda （\ x - > ...） x 的值应该是某个特定的值。为lambda内的 x 挑选一个值应该听起来很愚蠢，但这就是无法匹配等于等于，刚性类型变量，等等等等的错误。注意，即使不使用明确的 forall 量词，任何顶级类型签名都有一个隐含的 forall 为每个提到的类型变量。

当然，这不是你得到的错误。什么是转义类型变量意味着更加愚蠢 - 这就像有一个lambda （\ x - > ...）并试图使用 x outside lambda，独立于将其应用于参数。不，不会将lambda应用于某些内容并使用结果值 - 我的意思是实际在其定义的范围外使用变量本身。

这种情况可能发生在类型上（没有像使用lambda的例子那样明显荒谬），原因是有两个类型变量的概念在四处浮动：在统一过程中，有变量表示未定类型，然后通过类型推断与其他这样的变量进行识别。另一方面，你有上面描述的量化类型变量，它们被明确地确定为可能的类型。

考虑lambda表达式的类型（\ x - > x）。从一个完全不确定的类型 a 开始，我们看到它需要一个参数并将其缩小到 a - > b ，那么我们看到它必须返回与它的参数类型相同的东西，所以我们进一步缩小到 a - >一个。但现在它适用于任何类型的 a 您可能需要，所以我们给它一个量词（forall a。a - > a）统一

那个量词的范围。

---

显然，我忘了实际解释术语skolem类型变量在这里，嘿。正如评论中所提到的，在我们的案例中，它基本上是刚性类型变量的同义词，所以上面仍然解释了这个想法。

我并不完全确定这个词源于何处，但我猜想它涉及 Skolem规范形式，并用通用术语表示存在性量化，就像在GHC中所做的那样。 skolem（或刚性）类型的变量是在某个范围内由于某种原因具有未知但特定类型的变量 - 属于多态类型的一部分，来自存在性数据类型& c。

Eeek! GHCi found Skolems in my code!

...
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
...

What are they? What do they want with my program? And why are they trying to escape (the ungrateful little blighters)?

解决方案

To start with, a "rigid" type variable in a context means a type variable bound by a quantifier outside that context, which thus can't be unified with other type variables.

This works a great deal like variables bound by a lambda: Given a lambda (\x -> ... ), from the "outside" you can apply it to whatever value you like, of course; but on the inside, you can't simply decide that the value of x should be some particular value. Picking a value for x inside the lambda should sound pretty silly, but that's what errors about "can't match blah blah, rigid type variable, blah blah" mean.

Note that, even without using explicit forall quantifiers, any top-level type signature has an implicit forall for each type variable mentioned.

Of course, that's not the error you're getting. What an "escaped type variable" means is even sillier--it's like having a lambda (\x -> ...) and trying to use specific values of x outside the lambda, independently of applying it to an argument. No, not applying the lambda to something and using the result value--I mean actually using the variable itself outside the scope where it's defined.

The reason this can happen with types (without seeming as obviously absurd as the example with a lambda) is because there are two notions of "type variables" floating around: During unification, you have "variables" representing undetermined types, which are then identified with other such variables via type inference. On the other hand, you have the quantified type variables described above which are specifically identified as ranging over possible types.

Consider the type of the lambda expression (\x -> x). Starting from a completely undetermined type a, we see it takes one argument and narrow that to a -> b, then we see that it must return something of the same type as its argument, so we narrow it further to a -> a. But now it works for any type a you might want, so we give it a quantifier (forall a. a -> a).

So, an escaped type variable occurs when you have a type bound by a quantifier that GHC infers should be unified with an undetermined type outside the scope of that quantifier.

---

So apparently I forgot to actually explain the term "skolem type variable" here, heh. As mentioned in comments, in our case it's essentially synonymous with "rigid type variable", so the above still explains the idea.

I'm not entirely sure where the term originated from, but I would guess it involves Skolem normal form and representing existential quantification in terms of universal, as is done in GHC. A skolem (or rigid) type variable is one that, within some scope, has an unknown-but-specific type for some reason--being part of a polymorphic type, coming from an existential data type, &c.

这篇关于什么是skolems？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！