haskell - 逆变位置上较高等级类型的统一

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的类型 promise ，当被称为 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' 更通用)。