了解 Haskell 的 RankNTypes

Question

在使用 GHC 扩展程序时，我遇到了RankNTypes at the School of Haskell，它有以下示例：

main = print $ rankN (+1)

rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN f = (f 1, f 1.0)

文章为rankN提供了另一种类型：

rankN :: forall n. Num n => (n -> n) -> (Int, Double) 

区别的解释是

后一个签名需要一个从 n 到 n 的函数，对于一些 Num n；前一个签名要求每个 Num n 都有一个从 n 到 n 的函数。

我可以理解，前一种类型需要签名才能成为括号中的内容或更一般的内容。我不明白后一个签名只需要一个函数n -> n 用于“一些Num n”的解释。有人可以详细说明和澄清吗？你如何“阅读”这个以前的签名，让它听起来像它的意思？后一个签名是否与简单的Num n => (n -> n) -> (Int, Double) 相同而无需forall？

Answer 1

在rankN 的情况下，f 必须是对所有数字类型都有效的多态函数n。

在rank1 的情况下，f 只需为单个数字类型定义。

这里有一些代码可以说明这一点：

{-# LANGUAGE RankNTypes #-}

rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN = undefined

rank1 :: forall n. Num n => (n -> n) -> (Int, Double)
rank1 = undefined

foo :: Int -> Int  -- monomorphic
foo n = n + 1

test1 = rank1 foo -- OK

test2 = rankN foo -- does not type check

test3 = rankN (+1) -- OK since (+1) is polymorphic

更新

回应@helpwithhaskell 在 cmets 中的问题...

考虑这个函数：

bar :: (forall n. Num n => n -> n) -> (Int, Double) -> (Int, Double)
bar f (i,d) = (f i, f d)

也就是说，我们将f 应用于 Int 和 Double。不使用 RankNTypes 就不会进行类型检查：

-- doesn't work
bar' :: ??? -> (Int, Double) -> (Int, Double)
bar' f (i,d) = (f i, f d)

以下签名均不适用于???：

Num n => (n -> n)
Int -> Int
Double -> Double

Answer 2

在正常情况下（forall n. Num n => (n -> n) -> (Int, Double)），我们选择一个n首先然后提供一个函数。所以我们可以传入Int -> Int、Double -> Double、Rational -> Rational等类型的函数。

在等级 2 的情况下 ((forall n. Num n => n -> n) -> (Int, Double))，我们必须提供函数 before 我们知道 n。这意味着该函数必须为 any n 工作；我为上一个示例列出的示例都不起作用。

对于给出的示例代码，我们需要它，因为传入的函数 f 应用于两种不同的类型：Int 和 Double。所以它必须对他们俩都有效。

第一种情况是正常的，因为这是类型变量默认的工作方式。如果您根本没有forall，那么您的类型签名就相当于一开始就拥有它。 （这称为 prenex 形式。）所以Num n => (n -> n) -> (Int, Double) 隐含地与forall n. Num n => (n -> n) -> (Int, Double) 相同。

适用于any n 的函数类型是什么？正是forall n. Num n => n -> n。

Answer 3

你如何“阅读”这个以前的签名，让它听起来像它的意思？

你可以阅读

rankN :: (forall n. Num n => n -> n) -> (Int, Double)

因为“rankN 接受参数f :: Num n => n -> n”并返回(Int, Double)，其中f :: Num n => n -> n 可以读作“对于任何数字类型n，f 可以接受n 并返回@987654328 @"。

排名第一的定义

rank1 :: forall n. Num n => (n -> n) -> (Int, Double)

然后将被解读为“对于任何数字类型 n，rank1 接受一个参数 f :: n -> n 并返回一个 (Int, Double)”。

后一个签名是否与简单的Num n => (n -> n) -> (Int, Double) 相同而无需forall？

是的，默认情况下，所有 foralls 都隐式放置在最外层位置（导致 rank-1 类型）。