编程语言的类型系统计算机科学导论第三讲.pptVIP

* * * * * * * * * * * * * * * * * * * * * 多 态 类 型 多态函数定义的类型推断 根据函数体中的语句来推断多态函数的类型 deref (p) { //p的类型一无所知，暂定位p : ? return *p // 需要根据?* ? 的类型来计算 } ? 由编程语言知，?* ? : ??. pointer(?) ? ? ? 对*的上述出现，脱掉?，用新类型变量?，得 pointer(?) ? ?，再对? 和pointer(?)进行合一计算 ? 得? = pointer(?) ，即deref : pointer(? ) ? ? ? 再戴上?，得deref : ??. pointer(? ) ? ? 多 态 类 型 多态函数应用(application)的类型检查 检查表达式deref(deref (q )) (相当于**q)的类型， 其中q的类型是pointer(pointer(int)) 需要经过下面两步合一代换, 才能通过类型检查, 并得出结果类型int ? ?i代换成pointer(int) ? ?o代换成int apply : ?o derefo: pointer(?o) ? ?o apply : ?i derefi : pointer(?i) ? ?i q: pointer(pointer(int)) = pointer(int) = int 多 态 类 型 多态函数与重载函数的区别 在Ada语言中，可以定义如下二个函数： function “*”(i,j: integer) return complex;{ …} function “*”(x,y: complex) return complex; { …} 则算符*有三个函数，其类型分别是 integer ? integer ? integer（这是语言预定义的） integer ? integer ? complex complex ? complex ? complex “*”是重载函数: 根据实参类型选用不同的具体函数 deref是多态函数：一个函数适用于很多种实参类型 依 赖 类 型 对依赖类型的需求 类型集合：基本类型、类型构造符作用于若干类 型得到的构造类型 基于这种类型集合的类型系统，能否编写： ? 零向量构造函数zero_vector 应用到自然数n，得到长度为n的零向量 ? 较长向量构造函数cons 应用到长度为n的向量，得到长度为n+1的向量 ? 拼接向量的函数append 把长度为m和n的向量拼接成长度为m+n的向量 依 赖 类 型 依赖类型 依赖类型是指依赖于项的类型 若有类型构造符vector，应用于项n，vector(n)表示长度为n的所有向量构成的类型 这与类型构造符pointer应用于类型int，得到pointer(int)是不同的 先前三个函数的类型 ? zero_vector: ?n:nat. vector(n) ? cons: ?n:nat. data ? vector(n) ? vector(n+1) ? append: ?m:nat. ?n:nat. vector(m) ? vector(n) ? vector(m+n) 依 赖 类 型 依赖类型 用C可编写zero_vector: ?n:nat. vector(n)等函数： #include malloc.h long * zero_vactor(int n) { int i; long* p; p = malloc(n * sizeof(long)); for(i = 0; i n; i++) p[i] = 0; } 但编译器不认为所编函数有上述类型，而只看成 zero_vector : int ? pointer(long) 依 赖 类 型 无依赖类型给C编程带来的麻烦 以I/O函数为例，一个程序如下： #include stdio.h main() {printf(“%d, %d, %d\n”);} 编译器报告错误？运行时报告错误？若可正常运行，输出是什么？ 过去的（包括现在某些）编译器不报告错误，运行结果是输出3个整数，其值不能预知 现在的一些编译器（包括GCC 的高版本）给出警告错误： format ‘%d’ expects a matching ‘int’ argument 依 赖 类 型 无依赖类型给C编程带来的麻烦 难以完成spri