Mat*_*ick 66 haskell types type-variables
Eeek!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
...
这些是什么？他们对我的计划有什么要求？为什么他们试图逃脱(忘恩负义的小战士)？
C. *_*ann 53
首先,上下文中的"刚性"类型变量意味着由该上下文之外的量词限定的类型变量,因此不能与其他类型变量统一.
这很像是由lambda绑定的变量:给定一个lambda (\x -> ... ),从"外部"你可以将它应用到你喜欢的任何值,当然; 但在内部,你不能简单地决定价值x应该是某个特定的价值.x在lambda内部选取一个值应该听起来很傻,但这就是"无法与blah blah,刚性类型变量,blah blah匹配"的错误.
请注意,即使不使用显式forall量词,任何顶级类型签名forall对于提到的每个类型变量都是隐式的.
当然,这不是你得到的错误."转义类型变量"意味着什么甚至更愚蠢 - 它就像拥有一个lambda (\x -> ...)并尝试使用lambda x 外部的特定值,而不是将其应用于参数.不,不将lambda应用于某些东西并使用结果值 - 我的意思是实际上在它定义的范围之外使用变量本身.
这种情况可能发生在类型上(没有看起来像lambda这样的例子显然是荒谬的)是因为有两种"类型变量"概念浮动:在统一期间,你有"变量"代表未确定的类型,然后识别与其他此类变量通过类型推断.另一方面,您具有上述的量化类型变量,这些变量被特别标识为可能类型的范围.
考虑lambda表达式的类型(\x -> x).从完全未确定的类型开始a,我们看到它需要一个参数并将其缩小到a -> b,然后我们看到它必须返回与其参数相同类型的东西,因此我们将其进一步缩小到a -> a.但现在它适用于a您可能想要的任何类型,因此我们给它量词(forall a. a -> a).
因此,如果您有一个由量词约束的类型,GHC推断应该使用该量词范围之外的未确定类型进行统一,则会发生转义类型变量.
所以显然我忘了在这里解释"skolem型变量"一词,呵呵.正如评论中所提到的,在我们的例子中,它基本上与"刚性类型变量"同义,所以上面仍然解释了这个想法.
我不完全确定该术语的起源,但我猜它涉及Skolem正规形式并用通用的方式表示存在量化,就像在GHC中所做的那样.一个skolem(或刚性)类型变量是在某些范围内由于某种原因具有未知但特定类型的变量 - 属于多态类型的一部分,来自存在性数据类型,&c.
Mat*_*hid 25
据我了解,"Skolem变量"是一个与任何其他变量(包括其自身)不匹配的变量.
当您使用显式foralls,GADT和其他类型系统扩展等功能时,这似乎会在Haskell中弹出.
例如,请考虑以下类型:
data AnyWidget = forall x. Widget x => AnyWidget x
这说明你可以采用任何实现Widget类的AnyWidget类型,并将其包装成一个类型.现在,假设你试图解开这个:
unwrap (AnyWidget w) = w
嗯,不,你做不到.因为在编译时我们不知道w具有什么类型,所以没有办法为此编写正确的类型签名.这里的类型w已经"转义"了AnyWidget,这是不允许的.
据我了解,内部GHC提供w了一个Skolem变量类型,以表示它不能逃脱的事实.(这不是唯一的这种情况;还有一些其他地方由于输入问题导致某些值无法逃脱.)
pha*_*dej 10
当类型变量试图转义其范围时,会弹出错误消息.
我花了一段时间来弄清楚这一点,所以我会写一个例子.
{-# 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 有一种类型 SomeIi在LHS上有某种类型I z的类型z.由于forall量词,我们不得不引入新的(新的)类型变量.请注意,它不是通用的,因为它绑定在(SomeI i)表达式中.x用SomeI,这是确定的.所以unI应该有类型SomeI -> y.i因此,RHS也有类型I z.y和I z,但它注意到z在较低的背景下出台的.因此它失败了.否则类型unI将具有类型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