什么是斯科勒姆? [英] What are skolems?

问题描述

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

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.

这很像由 lambda 绑定的变量:给定一个 lambda (x -> ... )，从外部"你可以将它应用到任何你喜欢的值， 当然;但是在内部，您不能简单地决定 x 的值应该是某个特定值.在 lambda 中为 x 选择一个值听起来很傻，但这就是无法匹配等等，刚性类型变量，等等"的错误的意思.

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.

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

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

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

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.

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

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.

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

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

因此，当您的类型受量词绑定时，GHC 推断该类型应该与该量词范围之外的未确定类型统一.

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.

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

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.

我不完全确定该术语的来源，但我猜它涉及 Skolem 范式 并代表存在 通用量化，就像在 GHC 中所做的那样.skolem(或刚性)类型变量是在某个范围内由于某种原因具有未知但特定类型的变量——它是多态类型的一部分，来自存在的数据类型，&c.

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.

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