Вывод типа для решения проблемы унификации
-
20-08-2019 - |
Вопрос
Кто-нибудь знает, как решить проблему вывода типа?
E > hd (cons 1 nil) : α0
со средой набора текста
E={
hd : list(α1 ) → α1 ,
cons : α2 → list(α2 ) → list(α2 ),
nil : list(α3 ),
1 : int
}
можно перенести в задачу унификации?
Любая помощь будет очень признательна!
Решение
Во-первых, переименуйте переменные типа, чтобы ни одна из переменных в вашем выражении не конфликтовала с переменными в среде типизации.(В вашем примере это уже сделано, поскольку выражение ссылается на { 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
Радуйтесь, теперь вы знаете тип каждого подвыражения в исходном выражении.
(Справедливое предупреждение: я сам в некоторой степени дилетант в этих вопросах и вполне мог где-то допустить опечатку или случайно смошенничать.)