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

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

{-# 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, так почему же это не соответствует его требованиям? Я чувствую, что в моих рассуждениях есть какая-то ошибка, но я не могу понять...


types polymorphism haskell type-theory rank-n-types
person radrow    schedule 04.03.2020    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Тип 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 должно быть более общим, чем B').

person chi    schedule 05.03.2020
comment
Похоже, все изменится< /а>. Я не очень рад этому. - person dfeuer; 05.03.2020
comment
@dfeuer Я очень доволен этим. Включение не работает должным образом с зависимыми типами, а forall плавающее и глубокое создание экземпляров — это уродливые хаки, несовместимые с надлежащими неявными типами функций первого класса. - person András Kovács; 05.03.2020