Понимание Политипов в выводе типа Хиндли-Милнера

Я читаю статью Википедии о Hindley-Milner Type Inference пытается сделать из этого какой-то смысл. Пока это я понял:

Типы классифицируются как монотипы или политипы.
Монотипы далее классифицируются как константы типа (например, int или string) или переменные типа (например, α и β).
Константы типа могут быть конкретными типами (например, int и string) или конструкторами типов (например, Map и Set).
Переменные типа (например, α и β) ведут себя как заполнители для конкретных типов (например, int и string).

Теперь мне сложно понять политипы, но, изучив немного Haskell, я это сделаю:

Типы сами имеют типы. Формально типы типов называются видами (т.е. Существуют разные типы типов).
Конкретные типы (например, int и string) и переменные типа (например, α и β) имеют вид *.
Конструкторы типов (например, Map и Set) представляют собой лямбда-абстракции типов (например, Set имеет вид * -> * и Map имеет вид * -> * -> *).

То, что я не понимаю, это то, что означают отборочные. Например, что означает ∀α.σ? Я не могу изобразить головы или хвосты, и чем больше я читаю следующий абзац, тем больше смущает я:

Функция с политипом ∀α.α → α позволяет сопоставить любое значение одного и того же типа с самим собой, а функция идентификации является значением для этого типа. В качестве другого примера ∀α. (Set α) → int - это тип функции, отображающей все конечные множества в целые числа. Количество членов - это значение для этого типа. Обратите внимание, что квалификаторы могут отображаться только на верхнем уровне, т.е. Тип ∀α.α → ∀α.α, например, исключается синтаксисом типов и что монотипы включены в типы политипов, таким образом, тип имеет общий вид ∀α₁., ∀αₙ.τ.

Ответ 1

Во-первых, виды и полиморфные типы - это разные вещи. У вас может быть система типа HM, где все типы одного типа (*), вы также можете иметь систему без полиморфизма, но со сложными видами.

Если термин M имеет тип ∀a.t, это означает, что для любого типа s мы можем заменить s на a на t (часто пишем как t[a:=s], и мы будем что M имеет тип t[a:=s]. Это несколько похоже на логику, где мы можем заменить любой термин для универсально квантифицированной переменной, но здесь мы имеем дело с типами.

Именно это происходит в Haskell, только в Haskell вы не видите квантификаторы. Все переменные типа, которые появляются в сигнатуре типа, неявно определяются количественно, как если бы у вас был forall перед типом. Например, map будет иметь тип

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

и т.д.. Без этой неявной универсальной квантификации переменные типа a и b должны иметь некоторое фиксированное значение, а map не будет полиморфным.

Алгоритм HM различает типы (без кванторов, монотипов) и схемы типов (универсальные квантифицированные типы, политипы). Важно, что в некоторых местах он использует схемы типов (например, в let), но в других местах допускаются только типы. Это делает все приемлемым.

Я также предлагаю вам прочитать статью о System F. Это более сложная система, которая позволяет forall где угодно в типах (поэтому все, что есть только что названный тип), но тип вывода/проверки неразрешимый. Это может помочь вам понять, как работает forall. Система F подробно описана в Girard, Lafont и Taylor, Доказательства и типы.

Ответ 2

Рассмотрим l = \x -> t в Haskell. Это лямбда, которая представляет собой термин t с переменной x, который будет заменен позже (например, l 1, что бы это ни значило). Аналогично, ∀α.σ представляет тип с переменной типа α, то есть f : ∀α.σ, если функция параметризована типом α. В некотором смысле σ зависит от α, поэтому f возвращает значение типа σ(α), где α будет заменено в σ(α) позже, и мы получим некоторый конкретный тип.

В Haskell вам разрешено пропустить ∀ и определить функции так же, как id : a -> a. Причина того, что позволяет исключить квантификатор, в основном такова, что им разрешен только верхний уровень (без расширения RankNTypes). Вы можете попробовать этот фрагмент кода:

id2 : a -> a -- I named it id2 since id is already defined in Prelude
id2 x = x

Если вы спросите ghci для типа id (:t id), он вернет a -> a. Если быть более точным (более теоретиком типа), id имеет тип ∀a. a -> a. Теперь, если вы добавите в свой код:

val = id2 3

3 имеет тип Int, поэтому тип Int будет заменен на σ, и мы получим конкретный тип Int -> Int.