问题描述
最初我假设函数类型的 LHS 上的嵌套全称量词的范围可以纯语法确定,即 (forall a. a -> b) -> Bool
括号内的所有内容都在同一范围内。然而,这个假设是错误的:
{-# LANGUAGE RankNTypes #-}
fun :: (forall a. [a] -> b) -> Bool
fun _ = undefined
arg :: c -> c
arg _ = undefined
r = fun arg -- type variable a would escape its scope
这是有道理的,因为在 fun
中,b
必须在 a
之前选择,因此是固定的或独立于 a
。在统一期间,参数类型 c -> c
会强制 b
使用 [a0]
进行实例化。
所以也许类型级别的范围更像是术语级别的函数,其中结果值显然不是函数范围的一部分。换句话说,如果 b
不是函数类型的 codomain,类型检查器将通过。不幸的是,我无法提出支持我的推理的注释。
一种更严格的方法是禁止在统一期间使用任何灵活的相同注释实例化刚性类型变量。这两种方式对我来说似乎都是合法的,但这在 Haskell 中实际上是如何工作的?
解决方法
非量化类型变量在顶层隐式量化。你的类型相当于
$ sed 's/#master_finger: '\'\''/master_finger: '\''$(date)'\''/' file
master_finger: '$(date)'
因此,fun :: forall b . (forall a. [a] -> b) -> Bool
arg :: forall c . c -> c
的范围是整个类型。
您可以将每个 b
的变量视为函数接收的一种隐式附加类型参数。我想你明白,在像
forall
foo :: Int -> (String -> Bool) -> Char
值由 Int
的调用者选择,而 foo
值由 String
在调用作为第二个论点。
本着同样的精神,
foo
表示fun :: forall b. (forall a. [a] -> b) -> Bool
被b
的调用者选择,而fun
被a
自己选择。
调用者确实可以使用 fun
显式传递 b
类型并写入
TypeAnnotations
之后,必须传入 fun @Int :: (forall a. [a] -> Int) -> Bool
类型的参数,而 forall a. [a] -> Int
适合这种多态类型。
length
由于这是 fun @Int length :: Bool
的调用站点,我们无法看到“类型参数”fun
的传递位置。这确实只能在 a
的定义中找到。
好吧,事实证明实际上不可能定义一个 fun
,该类型对其参数(fun
,上面)进行有意义的调用。如果我们有一个稍微不同的签名,那就是这样:
length
在这里我们可以看到 fun :: forall b. Eq b => (forall a. [a] -> b) -> Bool
fun f = f @Int [1,2,3] /= f @Bool [True,False]
(通过调用绑定到 f
)在两种不同的类型上被调用了两次。这会生成两个 length
类型的值,然后可以将它们进行比较以生成最终的 b
。