Почему forall a. a не считается подтипом Int, хотя я могу использовать выражение типа forall a. ожидается какой-нибудь один из типов Int?

Ответ 1

В типизированных лямбда-исчислениях мы имеем отношение типизации, обычно обозначаемое как : или в Haskell как ::. В общем случае отношение "много для многих", поэтому тип может содержать несколько значений, а также значение может иметь много типов.

В частности, в системах полиморфного типа значение может иметь несколько типов. Например

map :: (a -> b) -> [a] -> [b]

но также

map :: (Int -> Int) -> [Int] -> [Int].

В таких системах типа (иногда) можно определить отношение к типам со значением "более общий тип, чем", type order. Если t ⊑ s, то t является более общим, чем s, что означает, что if M : t then также M : s, и правила типизации такой системы типов позволяют сделать это именно так. Или мы говорим, что s является специализацией t. Поэтому в этом смысле существует отношение subtyping типов.

Однако, когда мы говорим о подтипировании в объектно-ориентированных языках, мы обычно подразумеваем номинальный подтипирование, то есть мы объявляем, какие типы являются подтипами о чем, например, когда мы определяем наследование класса. Хотя в Haskell это свойство типов, независимо от любых объявлений. Например, любой тип является специализацией forall a . a.

Для системы типа Hindley-Milner, которая позволяет вводить тип и является базой для большинства функциональных языков, существует понятие основной тип: если выражение M имеет (любой) тип, то оно также имеет свой основной тип, а главный тип - наиболее общий тип всех возможных типов M. Ключевой особенностью является то, что алгоритм вывода типа HM всегда находит наиболее общий тип. Таким образом, наиболее общий, предполагаемый основной тип может быть специализирован для любого допустимого типа M.

Ответ 2

С таким вопросом я бы сделал шаг назад и сказал, что в основном математические теории, лежащие в основе дизайна Haskell, System F варианты, которые не имеют понятия подтипирования.

Да, можно взглянуть на синтаксис поверхности Haskell и заметить, что есть случаи, подобные тому, что вы поднимаете, где выражение какого-либо типа T может использоваться в любом контексте, где ожидается T'. Но это не происходит потому, что Haskell был разработан для поддержки подтипов. Скорее, это происходит как случайность того факта, что Haskell был разработан, чтобы быть более удобным для пользователя, чем точная передача системы F.

В этом случае это связано с тем, что кванторы уровня уровня обычно не написаны явно в коде Haskell, а типы lambdas и приложения уровня никогда не бывают. Если вы посмотрите на тип forall a. a из угла системы F, то подстановка в контексты Int исчезнет. a :: forall a. a - это функция уровня типа и не может использоваться в контексте, который ожидает Int - вам нужно сначала применить его к Int, чтобы получить a Int :: Int, а это то, что вы действительно можете использовать в Int контекст. Синтаксис Haskell скрывает это во имя удобства пользователя, но он присутствует в основной теории.

Итак, коротко, хотя вы могли бы проанализировать Haskell, указав, какие типы выражений можно подставить в какие типы контекстов и продемонстрировать, что существует какое-то отношение крипто-подтипа, это просто не полезно, потому что оно дает анализы, которые плавают против текущего дизайна. И это не столько вопрос технических вопросов, сколько намерений и других человеческих факторов.

Ответ 3

Вы правы, что типы значения типа forall a. a могут использоваться везде, где ожидается Int, и это подразумевает отношение подтипа между двумя типами. Другие ответы выше пытаются убедить вас в том, что эта "более полиморфная, чем" -реклама не является подтипированием. Однако, хотя это, безусловно, отличается от форм подтипирования, обнаруженных в типичных объектно-ориентированных языках, это не означает, что "более полиморфная", чем "отношение" не может рассматриваться как (другая) форма подтипирования. Фактически, некоторые формализации систем полиморфного типа моделируют именно это отношение в их подтипическом отношении. Так обстоит дело, например, в системе типов в Odersky и Läufer paper "Помещение аннотаций типа для работы" .

Ответ 4

Под :: a мы подразумеваем "Любой тип", но не подтип. a может быть Int, или Bool, или IO (Maybe Ordering), но не в частности. a не является типом, а переменной типа.

Скажем, у нас есть такая функция:

id x = x

Компилятор понимает, что для нашего аргумента x нет определенного типа. Мы можем использовать любой тип для x, пока он эквивалентен тому, что выходит из id. Итак, мы пишем подпись так:

--    /- Any type in...
--    |    /- ...same type out.
--    V    V
id :: a -> a

Помните, что типы начинаются с заглавной буквы в Haskell. Это не тип: это переменная типа!

Мы используем полиморфизм, потому что это проще сделать. Например, композиция - полезная идея:

(>>>) :: (a -> b) -> (b -> c) -> (a -> c)
(>>>) f g a = g (f a)

Итак, мы можем писать такие вещи, как:

plusOneTimesFive :: Int -> Int
plusOneTimesFive = (+1) >>> (* 5)

reverseHead :: [Bool] -> Bool
reverseHead = reverse >>> head

Но что, если мы должны были написать каждый тип следующим образом:

(>>>) :: (Bool -> Int) -> (Int -> String) -> (Bool -> String)
(>>>) f g a = g (f a)

(>>>') :: (Ordering -> Double) -> (Double -> IO ()) -> (Ordering -> IO ())
(>>>') f g a = g (f a)

(>>>'') :: (Int -> Int) -> (Int -> Bool) -> (Int -> Bool)
(>>>'') f g a = g (f a)

-- ...and so on.

Это было бы просто глупо.

Итак, компилятор выводит тип с использованием унификации типов:

Скажем, я ввожу это в GHCi. Скажем, 6 в Int для простоты здесь.

id 6

Компилятор думает: "id :: a -> a, и ему передается Int, поэтому a = Int, поэтому id 6 :: Int.

Это не подтипирование. Подтипирование можно было бы захватить с помощью классов, но это основной полиморфизм при игре.

Ответ 5

Это не подтипирование, это объединение типов!

a :: forall a. a
a = undefined

b :: Int
b = a

В b = a мы ограничиваем b и a одинаковым типом, поэтому компилятор проверяет, что это возможно. a имеет тип forall a. a, который по определению объединяется с каждым типом, поэтому компилятор выполняет наше ограничение.

Унификация типов также позволяет нам делать такие вещи, как:

f :: (a -> Int) -> a
g :: (String -> b) -> b
h :: String -> Int
h = f g

Пройдя через объединение, f :: (a -> Int) -> a означает, что g должен иметь тип a -> Int, что означает, что a -> Int должен объединиться с (String -> b) -> b, поэтому b must b должен быть Int, что дает g конкретный тип (String -> Int) -> Int, что означает a is String -> Int.

Ни a -> Int, ни (String -> b) -> b не является подтипом другого, но они могут быть унифицированы как (String -> Int) -> Int.