快速示例:
{-# LANGUAGE RankNTypes #-}
l :: (forall b. [b] -> [b]) -> Int
l f = 3
l1 :: forall a. a -> a
l1 x = x
l2 :: [Int] -> [Int]
l2 x = x
k :: ((forall b. [b] -> [b]) -> Int) -> Int
k f = 3
k1 :: (forall a. a -> a) -> Int
k1 x = 99
k2 :: ([Int] -> [Int]) -> Int
k2 x = 1000
m :: (((forall b. [b] -> [b]) -> Int) -> Int) -> Int
m f = 3
m1 :: ((forall a. a -> a) -> Int) -> Int
m1 x = 99
m2 :: (([Int] -> [Int]) -> Int) -> Int
m2 x = 1000
这里:
l l1
类型检查通过l l2
未能通过类型检查k k1
未能通过类型检查k k2
类型检查通过m m1
类型检查通过m m2
未能通过类型检查
虽然我对 l
和 m
的情况非常满意,但我不理解 k
部分。存在一种“更多态”的关系,例如forall a. a -> a
比 forall b. [b] -> [b]
更加多态,因为可以仅替换 a/[b]
。但为什么当多态类型位于逆变位置时,这种关系会翻转呢?
就像我看到的那样,k
期望“一个接受任何列表操作的机器并生成 Int 的机器”。 k1
是“接受任何恒等机器并生成 int 的机器”。 因此,k1
提供的比 k
要求的要多得多,那么为什么它不能符合其要求呢?我感觉我的推理有些错误,但我无法理解...
forall
浮动和深层实例化是丑陋的hack,与适当的一流隐式函数类型不兼容。 - András Kovács