在RankNTypes中forall的目的

Question

在帮助下编写一些Haskell代码时hlint,我按照提示向函数添加了类型签名.它注入了类似这样的东西:

{-# LANGUAGE RankNTypes #-}

multipleOf :: forall a. Integral a => a -> a -> Bool
multipleOf divisor n = n `mod` divisor == 0

这种语言扩展对我来说是新的,但据我所知,这与更简单的相同:

multipleOf :: Integral a => a -> a -> Bool
multipleOf divisor n = n `mod` divisor == 0

我读过的每个N级类型的例子似乎都没有在已经可用的多态上添加任何新东西,而且这种forall语法似乎没有添加任何值.

我错过了什么？forall除了没有扩展的可用语法之外,还有一个很好的例子吗？

Answer 1

您错过了可以限制量化类型变量的范围:

modifyPair :: (Num b, Num c) => (forall a. Num a => a -> a) -> (b, c) -> (b, c)
modifyPair f (b, c) = (f b, f c)

尝试编写没有RankNTypes扩展名的功能.特别是,允许​​该对的元素彼此不同.

这个具体的例子并不太有用,但一般的想法成立.您可以指定函数的参数必须是多态的.

您可以使用此工具执行其他技巧.规范的例子来自ST.该ST库的目标是允许有限使用可变数据.也就是说,您可以实现涉及真实变异的算法,并提供纯粹的外部接口.ST本身通过聪明的类型系统技巧来证明使用是安全的:

newtype ST s a    = ... -- details aren't important
newtype STRef s a = ... -- details still aren't important

-- a standard-ish interface to mutable data
newSTRef :: ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()

-- the magic using RankNTypes
runST :: (forall s. ST s a) -> a

额外的类型变量s值得关注.它出现在两者ST和STRef.每个操作a的函数STRef都会确保sin ST和STRef是同一个类型变量.因此,当您到达时runST,您会发现类型s必须与类型无关a.s它的范围比它的范围更受限制a.最终的结果是你不能写出类似的东西runST newSTRef.类型检查器将拒绝它,因为类型变量s必须转义它量化的上下文.

因此,当你可以指定函数的参数必须是多态的时,你可以提供一些方便的技巧.