Вывод типа к проблеме унификации
Кто-нибудь знает, как проблема вывода типа
E > hd (cons 1 nil) : α0
со средой набора текста
E = {
hd : list(α1 ) → α1 ,
cons : α2 → list(α2 ) → list(α2 ),
nil : list(α3 ),
1 : int
}
может быть перенесено в задачу унификации?
Любая помощь будет очень признательна!
Ответы 1
Сначала переименуйте переменные типа, чтобы ни одна из переменных в вашем выражении не конфликтовала с переменными в среде ввода. (В вашем примере это уже сделано, поскольку выражение ссылается на {a0}, а среда ввода ссылается на {a1, a2, a3}.
Во-вторых, используя переменные нового типа, создайте переменную типа для каждого подвыражения в вашем выражении, получая что-то вроде:
nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable
В-третьих, сгенерируйте набор уравнений среди переменных типа, которые должны выполняться. Вы можете делать это снизу вверх, сверху вниз или другими способами. См. Херен, Бастиан. Сообщения об ошибках высшего качества. 2005 г. для подробной информации о том, почему вы можете выбрать тот или иной путь. В результате получится что-то вроде:
a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)
// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params
a8 = list(a1) -> a1 // = E(hd)
// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param
Обратите внимание: если одна и та же функция использовалась из среды типов дважды, нам потребовалось бы больше переменных нового типа (на втором шаге выше) для объединения, чтобы случайно не сделать все вызовы cons, использующие один и тот же тип. . Я не знаю, как объяснить эту часть более четко, извините. Здесь мы находимся в простом случае, так как hd и cons используются только один раз.
В-четвертых, объедините эти уравнения, чтобы получить (если я не ошибся) что-то вроде:
a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int
Возрадуйтесь, теперь вы знаете тип каждого подвыражения в исходном выражении.
(Честно предупреждаю, я сам в некоторой степени любитель в этих вопросах, и я вполне мог допустить опечатку или случайно обмануть где-то здесь.)