在逆变位置上统一更高级别的类型

Question

快速示例：

{-# 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 想要的要多，那么为什么它不符合它的要求呢？我觉得我的推理有些错误，但我无法理解......

Answer 1

k 的类型承诺，当以k f 调用时，对f 的每次调用都将以(forall b. [b] -> [b]) 类型的函数作为参数。

如果我们选择f = k1，我们会传递一个forall a. a->a 类型的函数作为输入。当 k 使用不太通用的函数（(forall b. [b] -> [b]) 类型）调用 f = k1 时，这不会得到满足。

更具体地说，考虑一下：

k :: ((forall b. [b] -> [b]) -> Int) -> Int 
k f = f (\xs -> xs++xs)

k1 :: (forall a. a -> a) -> Int                            
k1 x = x 10 + length (x "aaa")

两种类型检查。然而，减少k k1 我们得到：

k k1 =
k1 (\xs -> xs++xs) =
(\xs -> xs++xs) 10 + length ((\xs -> xs++xs) "aaa") =
(10++10) + length ("aaa"++"aaa")

这是错误类型的，所以k k1 也必须是错误类型的。

因此，是的——逆变位置确实颠倒了子类型的顺序（又名“不那么普遍”）。为了使A -> B 比A' -> B' 更通用，我们希望前者对输入的要求更少（A 必须不如A' 通用）并为输出提供更多保证（B 必须比B' 更通用）。