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

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

2 голосов
/ 09 декабря 2008

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

E > hd (cons 1 nil) : α0

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

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

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

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

1 Ответ

2 голосов
/ 19 декабря 2008

Во-первых, переименуйте переменные типа, чтобы ни одна из переменных в вашем выражении не конфликтовала с переменными в среде ввода. (В вашем примере это уже сделано, поскольку выражение ссылается на {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

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

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

...