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

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 部分。存在某种 "more polymorphic" 的关系，例如 forall a. a -> a 比 forall b. [b] -> [b] 更具有多态性，因为可以只替换 a/[b]。 但是，如果多态类型处于逆变位置，为什么这种关系会翻转？

据我所知 k 预计 "a machine that takes machine operating on any lists that produces Int"。 k1 是 "a machine that takes any endomorphism-machine that produces 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 也必须是错误类型。

因此，是的——逆变位置确实颠倒了子类型化的顺序（又名 "being less general"）。为了让 A -> B 比 A' -> B' 更通用，我们希望前者对输入的要求更少（A 必须比 A' 更通用）并提供更多保证在输出上（B 必须比 B' 更通用）。

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

Unification of higher rank types on contravariant positions

haskell

types

polymorphism

type-theory

rank-n-types