逆变位置上的高阶类型的统一

Question

逆变位置上的高阶类型的统一

haskelltypespolymorphismtype-theoryrank-n-types

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

- radrow

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- chi · Accepted Answer

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")

这段文字涉及到it技术，其中提到了一个类型不正确的问题，所以k k1也必须是类型不正确的。

因此，确实——逆变位置确实会颠倒子类型（也称为“更不一般”）的顺序。对于A->B要比A' -> B'更一般，我们希望前者对输入提出更少的要求（A必须比A'更不一般），并在输出方面提供更多的保证（B必须比B'更一般）。