Я попытаюсь сделать это максимально механическим способом, точно так же, как это было бы реализовано в большинстве компиляторов.
Давайте разберем это:
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 применяется к результату (xz), который мы только что назвали 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
Мне было трудно найти хорошее объяснение этого процесса вывода и ограничения типа.Я использовал две книги, чтобы изучить его - «Реализация современного компилятора в ML» Эндрю Аппеля и «Типы и языки программирования» Пирса.Ни один из них не был полностью освещен для меня, но между ними я понял это.