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

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，当调用 as 时k f，每次调用f都会将类型为 的函数作为参数(forall b. [b] -> [b])。

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

更具体地说，考虑一下：

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'）。