74

哎呀！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
...

这些是什么？他们对我的程序有什么要求？他们为什么要逃跑（忘恩负义的小家伙）？

4

4 回答 4

58

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

这很像受 lambda 约束的变量：给定一个 lambda (\x -> ... )，当然，您可以从“外部”将它应用于您喜欢的任何值；但在内部，您不能简单地决定 的值x应该是某个特定值。在 lambda中选择一个值x听起来很愚蠢，但这就是“无法匹配等等等等，刚性类型变量，等等等等”的错误的意思。

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

当然，这不是你得到的错误。“转义类型变量”的含义甚至更加愚蠢——就像拥有一个 lambda(\x -> ...)并尝试使用lambdax 之外的特定值，而与将其应用于参数无关。不，不将 lambda 应用于某些东西并使用结果值——我的意思是实际上在定义它的范围之外使用变量本身。

类型会发生这种情况的原因（看起来不像使用 lambda 的示例那样明显荒谬）是因为有两个“类型变量”概念浮动：在统一期间，您有表示未确定类型的“变量”，然后确定这些类型通过类型推断与其他此类变量。另一方面，您有上面描述的量化类型变量，它们被明确标识为可能的类型。

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

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

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

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

于 2012-10-04T02:43:05.053 回答
23

据我了解，“Skolem 变量”是一个与任何其他变量（包括其自身）都不匹配的变量。

当您使用显式 foralls、GADT 和其他类型系统扩展等功能时，这似乎会在 Haskell 中弹出。

例如，考虑以下类型：

data AnyWidget = forall x. Widget x => AnyWidget x

这就是说，您可以采用任何实现Widget该类的类型，并将其包装成一个AnyWidget类型。现在，假设您尝试打开它：

unwrap (AnyWidget w) = w

嗯，不，你不能那样做。因为，在编译时，我们不知道类型w有什么，所以没有办法为此编写正确的类型签名。这里的类型w已经从 中“逃脱” AnyWidget，这是不允许的。

据我了解，GHC 在内部给出w了一个 Skolem 变量的类型，以表示它不能逃脱的事实。（这不是唯一的这种情况；还有一些其他地方由于打字问题而无法逃脱某个值。）

于 2012-10-04T08:06:44.080 回答
11

当类型变量试图逃脱其范围时，会弹出错误消息。

我花了一段时间才弄清楚这一点，所以我会写一个例子。

{-# LANGUAGE ExistentialQuantification #-}
data I a = I a deriving (Show)
data SomeI = forall a. MkSomeI (I a)

那么如果我们尝试写一个函数

 unI (MkSomeI i) = i

GHC 拒绝对该函数进行类型推断/类型检查。

为什么？让我们尝试自己推断类型：

  • unI是一个 lambda 定义，因此它的类型x -> y适用于某些类型x和y.
  • MkSomeI有一个类型forall a. I a -> SomeI
    • MkSomeI i有一个类型SomeI
    • i在LHS上有某种类型I z的类型z。由于forall量词，我们不得不引入新的（新鲜的）类型变量。请注意，它不是通用的，因为它绑定在(SomeI i)表达式中。
    • 因此我们可以将类型变量x与统一起来SomeI，这没关系。所以unI应该有类型SomeI -> y。
  • i因此在RHS上也有类型I z。
  • 此时 unifier 尝试统一yand I z，但它注意到z在较低的上下文中引入了 。因此它失败了。

否则 for 的类型unI将具有 type forall z. SomeI -> I z，但正确的类型是exists z. SomeI -> I z。然而，一个 GHC 不能直接代表。

同样，我们可以看到为什么

data AnyEq = forall a. Eq a => AE a
-- reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

作品。

内部的（存在）变量AE x不会逃逸到外部范围，所以一切正常。

我还在 GHC 7.8.4 和 7.10.1 中遇到了一个“功能”RankNTypes ，它本身是可以的，但是添加GADTs会触发错误

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

example :: String -> I a -> String
example str x = withContext x s
  where
    s i = "Foo" ++ str

withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x

因此，您的代码可能没有问题。可能是 GHC，它无法始终如一地解决所有问题。

编辑：解决方案是给s :: forall a. I a -> String.

GADTs打开MonoLocalBinds，这使得推断的类型s具有 skolem 变量，因此类型不是forall a. I a -> String，而是t -> String，被t绑定在错误的上下文中。见：https ://ghc.haskell.org/trac/ghc/ticket/10644

于 2015-07-16T13:34:46.200 回答
0

什么是Skolem？

一个存在量化变量，即它“具有刚性/具体类型，外部世界无法知道，但内部世界可以”。

那么如何使用 Skolems？

TL;博士

unwrapBroken (ExistentiallyTyped x) = x

unwrapOk (ExistentiallyTyped x) = useConstraint x

当 Skolem 有一些您关心的类型类的实例时，它们很有用。您可以（仅？）通过它的约束使用未包装的东西。

简而言之，这里是转义的 skolem (that awithin forall a. ExistentiallyTyped a)：

data ExistentiallyTyped = forall a. SomeConstraint a => ExistentiallyTyped a

unwrapBroken :: forall a. ExistentiallyTyped -> a  <---- what? how'd that `a` break out? not the same `a` as in ExistentiallyTyped
unwrapBroken (ExistentiallyTyped x) = x :: a  <---- not the same `a` as above!

你不能这样做，a从包装x :: a中量化ExistentiallyTyped，但想想a就行了unwrapBroken :: forall a. ...。现在它以某种方式被普遍量化了？！（警告，我认为这开始成为可能的Dependent Types，而 haskell 还没有……）。所以你告诉我这个函数可以返回Intor Stringor AnyFrigginThing？

不，但你可以x :: a通过它的约束来利用它：

unwrapOk :: ExistentiallyTyped -> ResultOfUseConstraint
unwrapOk (ExistentiallyTyped x) = useConstraint x

例如，当我想要一个共享某个类型类的类型列表时，我就使用了它：

notPossible :: HasBork a => [Proxy a]
notPossible = [Proxy @Thing1, Proxy @Thing2]
-- Error! expected a `Proxy a` but got a `Proxy Thing1`

所以与其：

data Borkable = forall a. HasBork a => Borkable a

borks :: [Borkable]
borks = [thing1, thing2]

later = useBork <$> borks
于 2021-02-04T23:34:36.423 回答