类型系统是比较偏理论的，但随着函数式语言（Ocaml, F#）以及动态语言（Python, PHP）等逐步流行，其重要性也逐步凸显。 常规的类型系统大家是很熟悉的，例如： 3：int， false： Boolean，其难点在于函数和对象类型，一般的静态语言，将函数看成一个可调用的特殊变量， 例如，用python的语言来讲：

   add = lambda x,y: x+y

 

那么add（3,4）的类型就是int * int -> int，而不再仅仅是一个函数。 那么类型理论到此为止也没有很复杂，而且很直观。  那么，其难点在什么地方呢？  首先，我们把目前的类型可以定义为

 

T :: =  c | x | T -> T   （C: 类型常量，如int boolean等， x,类型变量，T -> T： 函数类型，“->”前是参数，“->”后是返回类型）

 

这个是个简单的类型化lambda演算的类型系统，和我们常见的语言的类型是一致的，只不过对函数的类型进行了刻画。 我们要做的第一个扩展是支持高阶函数（higher order）函数，即支持函数本身作为变量，例如： Id = lambda x： x。 这个是个简单的返回自身的函数， 类型可以定义为：

Id : t -> t

 

那么，f= Id(Id), Id本身作为参数，那么f 的类型是什么呢？ 按照前面的定义，f输入一个函数，返回一个函数，则可定义为 f: (t -> t) -> (t -> t) 。 到目前为止，似乎也没有问题， 但是,不幸的是，并不是所有的函数都有类型的，例如： foo  = lambda x： x(x), 那么 g = foo(foo), 这个函数是没有类型的，确切地说，是一个不会终止的递归函数，那么类型系统应该能够判断出这个函数是不能被类型化的，并且不应该在实际的系统中采用，否则运行时会抛出异常。 大家可以在python的环境中尝试这个函数。

如果说higher order是第一个重要扩展，那么多态(polymorphic)就是第二个重要扩展，多态在面向对象和动态语言中随处可见，例如前面的add函数，完全可以写成这样 add(“hello”, “word”), 其类型是 string*string -> string. 那么add的类型到底是什么呢？ 不同的参数有不同的类型，通用一点就是这样： Πt: t*t -> t.解释为对所有的类型参数，输入两个t类型，返回一个t类型。 这样，我们的类型系统扩展为

          t :: =  c | x | t-> t

    σ ：：= t |Πt. σ 

目前支持多态和高阶函数，已经能够应付很多语言的类型了。那么如何推导这个系统的类型呢？ 这就需要用到 Unification算法。 例如: lambda x,y,z : x(y(z)) , 其对应的类型是什么呢？ 其类型是： （（a->b）*（c->a）*c ）-> b 。你能推导出来吗？ 有空下次再讲，:-)

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

上一篇：学习型多功能导盲杖——交大学生又一有趣创意
下一篇：新书出版 - 《NewBluePill:深入理解硬件虚拟机》