Вывод типа на проблему объединения

Question

Кто-нибудь знает, как проблема вывода типа

E > hd (cons 1 nil) : α0

с набором текста

                E={
                   hd : list(α1 ) → α1 ,
                   cons : α2 → list(α2 ) → list(α2 ),
                   nil : list(α3 ),
                   1 : int
                }

можно перенести в проблему объединения?

Любая помощь будет принята с благодарностью!

Answer 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

Обратите внимание, что если бы одна и та же функция использовалась дважды из среды типов, нам потребовалось бы объединить больше новых переменных типа (на втором шаге, описанном выше), чтобы не было случайного вызова всех вызовов аргументов с использованием одного и того же типа., Я не уверен, как объяснить эту часть более четко, извините. Здесь мы находимся в простом случае, поскольку hd и cons используются только один раз.

В-четвертых, объедините эти уравнения, в результате чего (если я не ошибся) что-то вроде:

a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int

Радуйтесь, теперь вы знаете тип каждого подвыражения в вашем исходном выражении.

(Честное предупреждение, я сам в этом вопросе любитель, и, возможно, я допустил опечатку или нечаянно обманул где-то здесь.)