4

The topic of Section 7.12.5 of the GHC Users Guide is higher rank polymorphism. There are some example valid types, among others:

f4 :: Int -> (forall a.a->a)

Now I wonder what this type means. I think it is the same as:

f4' :: forall a. Int -> a -> a

If this is so, can we generally mentally move forall like the above (that appears right of the rightmost arrow) to the left assuming that no type variable with the same name occurs in the rest of the type (but this could be dealt with renaming, simply)?

For example, the following would still be correct, wouldn't it:

f5 :: Int -> (forall a. (forall b. b -> a) -> a)
f5' :: forall a. Int -> (forall b. b -> a) -> a

Would be thankful for an insightful answer.

Background: In this talk about lenses by SPJ, we have:

type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

and then, when you compose them, you have such a lens type in the result. Therefore I just wanted to know whether my intuition is correct, that the forall in the result doesn't really matter - it just appears "accidentally" because of the type synonym. Otherwise, there must be some difference between the types for f4, f4'and f5, f5' above I would want to learn about.

Here is a ghci session:

Prelude> let f5 :: Int -> (forall a. (forall b. b -> a) -> a); f5 i f = f i
Prelude> :t f5
f5 :: Int -> (forall b. b -> a) -> a
Prelude>

Looks like GHC agrees with me, at least in this case .....

4

1 回答 1

4

f4在您的示例中，可以普遍量化，因为Int -> (forall a. a -> a)和forall a. Int -> (a -> a)本质上是相同的。

但是我们不能在这个 Rank2 类型中应用你的类比(forall a. a -> a) -> (forall b. b -> b)。这种类型与forall b. (forall a. a -> a) -> (b -> b). 但是将第一个 forall 移出 ( forall a b. (a -> a) -> (b -> b)) 从本质上改变了类型的语义。

f :: (forall a. a -> a) -> (forall b. b -> b) -- Rank 2
g :: forall a b. (a -> a) -> (b -> b)         -- Rank 1

要查看差异，您可以实例化为a，因此可以将类型函数传递g给g。另一方面，参数 to必须是普遍量化的（由函数类型之前的 forall 指定）并且应该适用于所有类型（这种函数的示例是）。IntInt -> Intfid

这是对更高等级类型的一个很好的解释。

于 2013-10-10T10:53:08.417 回答