RankNTypes和范围'forall'

Question

这些有什么区别？

{-# LANGUAGE RankNTypes #-}

f :: forall a. a -> Int
f _ = 1

g :: (forall a. a) -> Int
g _ = 1

特别是,为什么我会收到错误g ()？

ghci> f ()
1
ghci> g ()
<interactive>:133:3:
    Couldn't match expected type `a' with actual type `()'
      `a' is a rigid type variable bound by
          a type expected by the context: a at <interactive>:133:1
    In the first argument of `g', namely `()'
    In the expression: g ()
    In an equation for `it': it = g ()

ghci> f undefined
1
ghci> g undefined
1

Answer 1

f只是一个普通的多态Haskell98函数,除了forall明确写出.因此签名中的所有类型变量都是调用者可以选择的参数(没有任何约束); 在你的情况下它已经解决了a ~ ().

gOTOH的等级为2级.它要求其参数具有多态类型forall a . a.()没有这种类型,它是单形的.但是如果我们再次添加显式,那么undefined这种类型(实际上只有未定义和错误等)forall.

也许通过一个不那么简单的Rank2函数变得更清晰:

h :: (forall a . (Show a, Num a) => a) -> String
h a = show a1 ++ " :: Double\n"
     ++ show a2 ++ " :: Int"
 where a1 :: Double; a2 :: Int
       a1 = a; a2 = a

GHCi> putStrLn $ h 4
4.0 :: Double
4 :: Int

但我不能这样做

GHCi> putStrLn $ h(4 :: Integer)

<interactive>:4:15:
    无法
    从上下文所
      期望的类型绑定的上下文(Show a,Num a)中推导出(a~Integer):(显示a, Num a)=> a
      at <interactive>:4:12-27`a
      '是一个刚性类型变量,
          由上下文预期的类型绑定:(显示a,Num a)=> a
          at <interactive>:4: 12
    在`h'的第一个参数中,即`(4 :: Integer)'
    在`($)'的第二个参数中,即`h(4 :: Integer)'
    在表达式中:putStrLn $ h(4: : 整数)

Answer 2

可以将其forall视为匿名类型函数.Haskell中其类型签名中具有类型变量的所有数据类型都隐式具有forall.例如考虑:

f :: a -> Int
f _ = 1

上面的函数f接受任何类型的参数并返回一个Int.它a来自哪里？它来自forall量词.因此它相当于:

f :: (forall a . a -> Int)
f _ = 1

的forallquatifier可用于任何类型的数据,而不仅仅是功能.例如,考虑以下值的类型:

() :: ()
10 :: Int
pi :: Floating a => a

这里()和10是单形的(即它们只能是一种具体的类型).另一方面pi是具有类型类约束的多态(即,只要该类型是其实例,它可以是任何类型Floating).pi明确写出的类型是:

pi :: (forall a . Floating a => a)

再次forall量词的作用就像一个类型的功能.它为您提供了类型变量a.现在考虑功能的类型g:

g :: (forall a . a) -> Int
g _ = 1

这里g需要一个类型的参数forall a . a并返回一个Int.这是g ()不起作用的原因:()是类型(),而不是类型forall a . a.实际上,唯一的类型值forall a . a是undefined:

undefined :: a

明确写出forall:

undefined :: (forall a . a)

如果你注意到我总是在forall量化周围加上括号.我这样做的原因是为了向您展示当您forall对函数使用量化时,量化一直延伸到右侧.这就像一个lambda:如果你没有在lambda周围加上括号,Haskell会将lambda函数一直扩展到右边.因此,f是(forall a . a -> Int)和否的类型(forall a . a) -> Int.

请记住,在第一种情况下,Haskell期望参数的类型a(即任何东西).但是在第二种情况下,Haskell期望参数的类型是(forall a . a)(即undefined).当然,如果您尝试评估,undefined那么您的程序将立即停止并出现错误.幸运的是,你不是要评估它.