Получение выражения типа в ML
Все,
Я хочу получить выражение типа для функции ниже в ML:
fun f x y z = y (x z)
Теперь я знаю, что ввод того же генерировал бы выражение типа. Но я хочу получить эти значения вручную.
Кроме того, упомяните общие шаги для следования при получении выражений типа.
3 ответа
Я попытаюсь сделать это наиболее механическим способом, точно так, как это реализовано в большинстве компиляторов.
Давайте разложим это на части:
fun f x y z = y (x z)
Это в основном сахар для:
val f = fn x => fn y => fn z => y (x z)
Добавим некоторые метасинтаксические переменные типа (это не настоящие SML-типы, просто держатели для данного примера):
val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5
Хорошо, мы можем начать генерировать систему ограничений из этого. T5 - это конечный тип возврата f. На данный момент мы будем называть конечный тип всей этой функции "TX" - некоторая свежая, неизвестная переменная типа.
Итак, вещь, которая будет генерировать ограничения в приведенном вами примере, - это применение функции. Она говорит нам о типах вещей в выражении. Фактически, это единственная информация, которая у нас есть!
Итак, что нам говорят приложения?
Игнорируя переменные типа, которые мы назначили выше, давайте просто посмотрим на тело функции:
y (x z)
z не применяется ни к чему, поэтому мы просто посмотрим, какой тип переменной мы назначили ей ранее (T4), и используем это как тип.
x применяется к z, но мы еще не знаем его тип возврата, поэтому создадим для него новую переменную типа и используем тип, который мы присвоили x (T2) ранее, чтобы создать ограничение:
T2 = T4 -> T7
y применяется к результату (x z), который мы только что назвали T7. И снова, мы еще не знаем тип возврата y, поэтому просто дадим ему свежую переменную:
T3 = T7 -> T8
Мы также знаем, что тип возврата y является типом возврата для всего тела функции, которую мы ранее назвали "T5", поэтому добавим ограничение:
T5 = T8
Для компактности, я немного упрощу это и добавлю ограничение для TX, основанное на том факте, что есть функции, возвращаемые функциями. Это можно вывести точно таким же методом, только он немного сложнее. Надеюсь, вы сможете сделать это самостоятельно в качестве упражнения, если не уверены, что в итоге мы получим это ограничение:
TX = T2 -> T3 -> T4 -> T5
Теперь соберем все ограничения:
val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5
TX = T2 -> T3 -> T4 -> T5
T2 = T4 -> T7
T3 = T7 -> T8
T5 = T8
Начнем решать эту систему уравнений, заменяя левые стороны правыми в системе ограничений, а также в исходном выражении, начиная с последнего ограничения и двигаясь к вершине.
val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T8
TX = T2 -> T3 -> T4 -> T8
T2 = T4 -> T7
T3 = T7 -> T8
val f : TX = fn (x : T2) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = T2 -> (T7 -> T8) -> T4 -> T8
T2 = T4 -> T7
val f : TX = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = (T4 -> T7) -> (T7 -> T8) -> T4 -> T8
val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8 = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
Хорошо, на данный момент это выглядит ужасно. На самом деле нам не нужен весь текст выражения - он был здесь только для того, чтобы внести некоторую ясность в объяснение. В основном в таблице символов у нас будет что-то вроде этого:
val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8
Последний шаг - обобщить все переменные типа, которые остались, в более привычные полиморфные типы, которые мы знаем и любим. По сути, это просто проход, заменяющий первую несвязанную переменную типа на 'a, вторую на 'b и так далее.
val f : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
И я уверен, что вы найдете тип, который ваш компилятор SML предложит для этого термина. Я делал это вручную и по памяти, так что прошу прощения, если я где-то что-то напутал :p
Мне было трудно найти хорошее объяснение этого процесса вывода и ограничения типов. Я использовал две книги для изучения этого процесса - 'Modern Compiler Implementation in ML' Эндрю Аппеля и 'Types and Programming Languages' Пирса. Ни одна из них не была для меня полностью просветляющей, но между ними двумя я разобрался.
Другой способ объяснить вывод типа состоит в том, что каждому (под) выражению и каждому (под) шаблону присваивается переменная типа.
Затем каждая конструкция в программе имеет уравнение, связывающее те переменные типа, которые имеют отношение к этой конструкции.
Например, если программа содержит f x и 'a1 - это переменная типа для f, и' a2 - переменная типа для x, и 'a3 - это переменная типа для "f x"
, тогда приложение приводит к уравнению типа: 'a1 =' a2 -> 'a3
Затем вывод типа в основном включает решение набора уравнений типа для объявления. Для машинного обучения это делается просто с помощью унификации, и это довольно легко сделать вручную.
Чтобы определить тип чего-то, нужно посмотреть на каждое место, где это используется. Например, если вы видите val h = hd l, вы знаете, что l - это список (потому что hd принимает список в качестве аргумента), и вы также знаете, что тип h - это тип, в котором l - список. Итак, допустим, что тип h - это a, а тип l - это a list (где a - это заполнитель). Теперь, если вы видите val h2 = h*2, вы знаете, что h и h2 - это intы, потому что 2 - это int, вы можете умножить int на другой int, а результат умножения двух int - это int. Поскольку ранее мы говорили, что тип h равен a, это означает, что a равен int, поэтому тип l равен int list.
Итак, давайте разберемся с вашей функцией:
Рассмотрим выражения в порядке их вычисления: Сначала выполняется x z, то есть x применяется к z. Это означает, что x - функция, поэтому она имеет тип a -> b. Так как z дается как аргумент функции, она должна иметь тип a. Поэтому тип x z - b, так как это тип результата x.
Теперь y вызывается с результатом x z. Это означает, что y также является функцией, и ее тип аргумента - тип результата x, то есть b. Поэтому y имеет тип b -> c. И снова тип выражения y (x z) - c, потому что это тип результата y.
Поскольку это все выражения в функции, мы не можем ограничивать типы дальше, и поэтому наиболее общие типы для x, y и z являются 'a -> 'b, 'b -> 'c и 'a соответственно, а тип всего выражения - 'c.
Это означает, что общий тип f - ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
О том, как типы выводятся программно, читайте в Hindley-Milner type inference.