|||
类型系统是比较偏理论的,但随着函数式语言(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 。你能推导出来吗? 有空下次再讲,:-)
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-10-20 01:43
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社