上次说到: lambda x,y,z : x(y(z)) , 其对应的类型是什么呢？ 

这里面的z可以看作一个普通变量（也可能是一个函数），y和x肯定是一个函数变量。 假定z的类型是c，则y(z)的类型是a， 那么y的类型为c->a， 则y(z)作为x函数的参数，假定x(y(z))的类型为b，那么x的类型为：a->b , 这里a为参数y(z)的类型，b为x(y(z))的类型， 那么整个函数的类型是输入x：a->b,y:c->a,z:c三个变量的类型，产生为类型为b的结果，则该函数类型为 （（a->b）*（c->a）*c ）-> b 

 

上面这个过程没有用到unification的算法，是从最里面开始倒推类型。对于自动化算法，其原理是一样的，只不过预先设置了类型变量，然后用等价替换来代替。例如，对于y(z)的类型推理，对于y和z各产生一个类型变量，例如m和n，则对于函数作用y(z)的表达式，则产生一个类型变量k， 那么现在有y:m, z:n, y(z);k，则对于y(z),有如下等式成立：  m = n->k, 因为y作为一个函数，输入一个n的参数，得到一个k的结果，所以y的类型m应该等价于n->k。

由此反复引用如上法则，则可以推导出所有变量的类型。 Unification的算法有两类，一类是简单的变量替换法（Hindley-Milner算法，简称HM算法[1]），一类是constraint/solve分离的方法（以Wand算法为代表[2]）。算法本身不是很复杂，但比较难写，就省略了。

这些算法都能处理前面提到的多态和高阶函数的类型，并且能够解决递归函数的类型，例如前面提到foo  = lambda x： x(x) 这个函数类型是(((a->b)->b)->b)，其中（a = a->b）,所以可以写成a->b的形式，采用a->b代替a，也可以写成(a->b)->b等一系列无穷循环的形式，比较好的写法是((a->b as a）->b, Ocaml采用这种写法)。 但g = foo(foo)是没有类型的，采用一个循环检测的技巧，可以把这种没有类型的函数找出来。如果你能理解Unification算法，可以针对这两个例子，看看如何推导他们的类型。

那么Unification算法有什么缺陷呢？ 不能处理什么情况呢？ 在类型系统里面有一个不动点算子，例如：list = fix(x) : unit+x*list, 这里定义了一个递归列表list,要么为空unit，那么为1个元素x，链接上一个列表。 通过这种构造方法，可以构造一个无穷的递归列表。如果x为一个普通类型（Monomorphic）的函数，则采用unification算法可以推出类型，如果允许为多态类型（polymorphic），则没有一个确定算法来推导这个类型，在理论上也称为Microft-Milner类型系统，（简称MM类型系统），Unification算法一定会终止，但MM类型系统的推理算法不一定终止，所以成为semi-unification算法。在实践中基本上都能终止，所以在一些类型推理里面还可以使用。不过现实的语言不大有这种复杂的类型，一般的c/c++/java采用unification算法就够了。对于一些比较偏理论的函数式语言例如ocaml，一般采用unification的变体。随着对cps计算风格的流行，说不定需要这种能够处理多态的不动点类型。关于semi-unification算法的推导，下次再讲。

参考文献：

[1] Ian Grant，Hindley-Milner Type Inference，http://ian-grant.net/hm/hindley-milner.pdf。 这个总结不错，并提供了源代码

[2] M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, 10:115–122, 1987.

转载本文请联系原作者获取授权，同时请注明本文来自戚正伟科学网博客。
链接地址：https://m.sciencenet.cn/blog-279072-465788.html

上一篇：新书出版 - 《NewBluePill:深入理解硬件虚拟机》
下一篇：AEVIOU蜂窝式中文滑行输入法获得全国大学生“挑战杯”特等奖