Почему это так. a не считается подтипом Int, в то время как я могу использовать выражение для типа a. ожидается где-нибудь один из типа Int?
Рассмотрим следующую пару определений функций, которые проходят проверку типов:
a :: forall a. a
a = undefined
b :: Int
b = a
Т.е. выражение типа forall a. a может быть использован, когда один из типа Int ожидается. Это мне кажется очень похожим на подтипирование, но утверждается, что системе типов в Haskell не хватает подтипов. Чем отличаются эти формы замещаемости?
Этот вопрос не относится к forall a. a, Другие примеры включают в себя:
id :: forall a. a -> a
id x = x
idInt :: Int -> Int
idInt = id
5 ответов
В типизированных лямбда-исчислениях мы имеем отношение типирования, обычно обозначаемое как : или в Хаскеле как ::, В общем случае отношение "многие ко многим", поэтому тип может содержать несколько значений, а также значение может иметь много типов.
В частности, в системах с полиморфным типом значение может иметь несколько типов. Например
map :: (a -> b) -> [a] -> [b]
но также
map :: (Int -> Int) -> [Int] -> [Int].
В таких системах типов (иногда) возможно определить отношение типов со значением "более общий тип, чем", порядок типов. Если t ⊑ s затем t является более общим, чем sЭто означает, что если M : t тогда также M : sи правила набора такой системы типов позволяют сделать вывод именно об этом. Или мы говорим, что s это специализация t, Таким образом, в этом смысле существует отношение подтипов к типам.
Однако, когда мы говорим о подтипах в объектно-ориентированных языках, мы обычно подразумеваем номинальные подтипы, то есть мы объявляем, какие типы являются подтипами того, что, например, когда мы определяем наследование классов. Находясь в Haskell, это свойство типов, не зависящее от каких-либо объявлений. Например, любой тип является специализацией forall a . a,
Для системы типов Хиндли-Милнера, которая допускает вывод типов и которая является основой для большинства функциональных языков, существует понятие основного типа: если выражение M имеет (любой) тип, то он также имеет свой основной тип, и основной тип является наиболее общим типом из всех возможных типов M, Ключевой особенностью является то, что алгоритм вывода типа HM всегда находит наиболее общий тип. Таким образом, наиболее общий выводимый основной тип может быть специализирован для любого допустимого типа M,
С таким вопросом я бы сделал шаг назад и сказал бы, что, по сути, математические теории, лежащие в основе дизайна Хаскелла, являются вариантами Системы F, которые не имеют концепции подтипирования.
Да, можно взглянуть на поверхностный синтаксис Хаскелла и заметить, что есть такие случаи, как то, что вы упоминаете, где выражение какого-то типа T может быть использован в любом контексте, где T' ожидается. Но это не возникает, потому что Haskell был разработан для поддержки подтипов. Скорее, это происходит как случайность того факта, что Haskell был разработан, чтобы быть более удобным для пользователя, чем точный рендеринг System F.
В этом случае это связано с тем фактом, что квантификаторы на уровне типов обычно не пишутся явно в коде на Haskell, а лямбды и приложения на уровне типов никогда не пишутся. Если вы посмотрите на тип forall a. a с точки зрения системы F, заменяемость в Int контексты уходят. a :: forall a. a является функцией уровня типа и не может использоваться в контексте, который ожидает Int- сначала нужно применить его к Int получить a Int :: Intто, что вы можете использовать в Int контекст. Синтаксис Haskell скрывает это во имя удобства для пользователя, но он есть в основной теории.
Короче говоря, хотя вы можете анализировать Haskell, табулируя, какие типы выражений можно подставить в какие типы контекста, и продемонстрировать, что существует какая-то крипто-подтипная связь, это просто не плодотворно, поскольку дает результаты анализа, которые соответствуют текущему проекту., И дело не столько в технических деталях, сколько в намерениях и других человеческих факторах.
Вы правы, что вводит значение типа forall a. a можно использовать везде, где Int ожидается, и что это подразумевает связь подтипа между двумя типами. Другие ответы, приведенные выше, пытаются убедить вас, что это отношение "более полиморфный, чем" не является подтипом. Однако, хотя он, безусловно, отличается от форм подтипирования, встречающихся в типичных объектно-ориентированных языках, это не означает, что отношение "более полиморфный, чем" не может рассматриваться как (другая) форма подтипа. Фактически, некоторые формализации систем полиморфного типа моделируют именно это отношение в их отношении подтипа. Так обстоит дело, например, в системе типов в работе Одерского и Лойфера "Использование аннотаций типов".
От :: 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,
Это не подтип. Подтип может быть захвачен с использованием классов типов, но это основной полиморфизм в игре.
Это не подтип, это объединение типов!
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 должен b должно быть Int, который дает g конкретный тип (String -> Int) -> Int, что значит a является String -> Int,
ни a -> Int ни (String -> b) -> b является подтипом другого, но они могут быть объединены как (String -> Int) -> Int,