关于Hindley-Milner算法，类型构造函数是什么意思？

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

如果您将其视为仅基于HM的简单syntactic unification（=/2），然后使用prolog。

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

所以A与B统一B与b(c)结合在一起>
[=/2意味着=是一个带有两个参数的运算符，并将返回将两个项或false统一的结果。
其他示例
?- a(A,b(c)) = a(A,A).
A = b(c).

?- a(b(d),b(c)) = a(A,A).
false.
如果您想通过Prolog在线尝试使用SWISH。