5

快速示例：

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

4

1 回答 1

4

k承诺的类型，当调用 as 时k f，每次调用f都会有一个 type 的函数作为参数(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'）。

于 2020-03-05T00:18:05.780 回答