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

Я читаю статью в Википедии о Hindley– Вывод типа Милнера пытается разобраться в этом. Пока что я понял:

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

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

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

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

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


type-inference type-systems haskell hindley-milner lambda-calculus
person Aadit M Shah    schedule 19.03.2013    source источник

Ответы (2)


arrow_upward
19
arrow_downward

Во-первых, виды и полиморфные типы - разные вещи. У вас может быть система типов 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 and Taylor, Доказательства и типы.

person Petr    schedule 19.03.2013
comment
Что касается количественной оценки типов в Haskell, полезным открытием может стать обзор экзистенциальных типов. - person ulidtko; 19.03.2013
comment
Вывод типа для Системы F неразрешим, но проверка типов проста (если под проверкой типа мы подразумеваем, что термины аннотированы типами, и мы просто проверяем, что эти аннотации имеют смысл). - person augustss; 19.03.2013
comment
@augustss Под проверкой типов подразумевается, что вам предоставляется неаннотированный термин (стиль Карри) и тип, и вы должны определить, соответствует ли термин типу или нет. Это тоже неразрешимо, как доказал Джо Уэллс в статье Типизация и тип Проверка в лямбда-исчислении второго порядка эквивалентна и неразрешима. - person Petr; 19.03.2013
comment
@ PetrPudlák Я знаю, что это неразрешимо. Многие люди относятся к проверке типов как к процессу проверки допустимости термина в церковном стиле, поэтому я хотел уточнить. - person augustss; 19.03.2013

arrow_upward
4
arrow_downward

Рассмотрим 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 о типе _19 _ (_ 20_), он вернет a -> a. Чтобы быть более точным (более теоретическим типом), id имеет тип ∀a. a -> a. Теперь, если вы добавите в свой код:

val = id2 3

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

person karlicoss    schedule 19.03.2013