Объединение типов высшего ранга на контравариантных позициях - PullRequest
Новая
       81

Объединение типов высшего ранга на контравариантных позициях

4 голосов
/ 05 марта 2020

Быстрый пример: 

{-# 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. Существует какая-то связь «больше полиморфных c», например, forall a. a -> a больше полиморфных c, чем forall b. [b] -> [b], потому что можно просто заменить a/[b]. Но почему это отношение переворачивается, если типы polymorphi c находятся на противоположных позициях?

Как я вижу k ожидает "машину, которая принимает машину, работающую с любыми списками, которая производит Int ». k1 - это «машина, которая принимает любую машину эндоморфизма, которая производит int». Поэтому k1 предлагает гораздо больше, чем хочет k, так почему же он не соответствует его требованиям? Я чувствую, что в моих рассуждениях есть какая-то ошибка, но я не могу ее понять ...

1 Ответ

3 голосов
/ 05 марта 2020

Тип k обещает, что при вызове 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 must быть более общим, чем B').

...