Что касается алгоритма Хиндли-Милнера, что означает конструктор типов?

Question

Скажем, у меня есть буквы A, B, представляющие переменные типа, которые изначально не связаны, и a,b,c, представляющие конструкторы типов. Затем мне нужно показать привязки переменных типа, полученные в результате объединения (или объяснить, почему в случае неудачи).

У меня есть следующая пара типов:

a(A,b(c)) and a(B,A)

У меня есть два вопросы:

1) Что они подразумевают под конструктором типа? для меня это; a(A,b(c)), похоже, a это конструктор типа, который представляет собой функцию, принимающую два параметра.

2) Может кто-нибудь показать мне, какой подход они выберут? Я посмотрел здесь, чтобы понять концепцию: http://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm

Answer 1

Если вы посмотрите на это как на простое syntacti c объединение ( = / 2 ), на котором основан HM, то используйте пролог .

?- a(A,b(c)) = a(B,A).
A = B, B = b(c).

поэтому A объединяется с B
и B объединяется с b(c)

---

=/2 означает, что = является оператором, который принимает два аргумента и вернет результат объединения двух терминов или ложного.

---

Некоторые другие примеры

?- a(A,b(c)) = a(A,A).
A = b(c).

?- a(b(d),b(c)) = a(A,A).
false.

---

Если вы хотите попробовать их онлайн с помощью Пролога, используйте SWI SH.