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

编程语言的类型系统计算机科学导论第三讲计算机科学技术学院陈意云[e-mail]课程内容•课程内容围绕学科理论体系中的模型理论,程序理论和计算理论1.模型理论关心的问题给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力2.程序理论关心的问题–给定模型M，如何用模型M解决问题–包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3.计算理论关心的问题给定模型M和一类问题,解决该类问题需多少资源讲座提纲•了解类型系统的重要性–围绕数组类型的若干实例来解释这个重要性•基本知识–类型表达式、定型断言、定型规则、类型系统•多态类型–多态函数、类型变量、多态函数的类型推断和类型检查•依赖类型–依赖类型的实例、编程语言中使用依赖类型的状况了解类型系统的重要性•一点个人评论(对发行量最大那本C程序设计教材)–对类型和类型系统介绍不足未强调变量、表达式和函数等都具有类型未强调各种运算对操作的对象和结果的类型都有规定–例1：完全没有把数组看成类型inta[3]：a未被看成元素类型为int、大小为3的数组类型的一个元素inta[4][3]：a未被看成以上述数组类型为元素类型、大小为4的数组类型的一个元素–例2：类型声明typedef被忽视(简略介绍在最后)了解类型系统的重要性•一点个人评论(对发行量最大那本C程序设计教材)–例3:读者难以理解编译器就下面代码报告的错误longa[10][10];main(){*(a+1)=a+1;}错误：incompatibletypeswhenassigningto‘longint[10]’fromtype‘longint(*)[10]’–计算机专业的新生从该书能较好地学习程序设计,但难以同时了解怎样学习编程语言下面举例说明了解类型系统的重要性了解类型系统的重要性•例1–在C中称&为地址运算符，&a为变量a的地址–数组名代表数组第一个元素的地址问题：如果a是一个数组名，那么表达式a和&a的值都是数组a第一个元素的地址，它们的使用是否有区？解答：用4个C文件在编译时获得的程序错误信息或运行结果来提示了解类型系统的重要性文件1：typedefintA[10][20];Aa;A*fun(){return(a);}该函数在Linux上用GCC编译，报告的错误如下：第4行：warning:returnfromincompatiblepointertype解释：表达式a的类型不是A的指针类型了解类型系统的重要性文件2：typedefintA[10][20];Aa;A*fun(){return(&a);}该函数在Linux上用GCC编译时，没有错误解释：表达式&a的类型是A的指针类型了解类型系统的重要性文件3：typedefintA[10][20];typedefintB[20];Aa;B*fun(){return(a);}该函数在Linux上用GCC编译时，没有错误解释：表达式a的类型是B(即A的元素的类型)的指针类型了解类型系统的重要性文件4：typedefintA[10][20];Aa;fun(){printf(“%d,%d,%d\n”,a,a+1,&a+1);}main(){fun();}该程序的运行结果是：（sizeof(int)是4字节）134518112,134518192,134518912解释：表达式a和&a的含义是有区别的：它们的类型不同了解类型系统的重要性结论由声明inta[i]，把a的类型表示为array(0..i–1,int)由声明int*p，把p的类型表示为pointer(int)则对一个t类型的数组a[i1][i2]…[in]来说，表达式a的类型是：pointer(array(0..i2–1,…array(0..in–1,t)…))表达式&a的类型是：pointer(array(0..i1–1,…array(0..in–1,t)…))array(…)和pointer(…)称为类型表达式了解类型系统的重要性•例2下面是一个C语言文件的内容longa1[10][10][10];longa2[][10][10];longa3[][][10];voidf(longa4[][10][10]){a1[2][2][2]=a4[2][2][2];}main(){f(a1);}GCC编译器对第2行给出警告：array‘a2’assumedtohaveoneelement[enabledbydefault]对第3行报告错误：arraytypehasincompleteelementtype了解类型系统的重要性•例2下面是一个C语言文件的内容longa1[10][10][10];longa2[][10][10];longa3[][][10];voidf(longa4[][10][10]){a1[2][2][2]=a4[2][2][2];}main(){f(a1);}–为什么第2行给出警告，而第3行报告错误？a2的元素是1010的长整型数组，但大小未确定a3的元素的类型定义不完全了解类型系统的重要性•例2下面是一个C语言文件的内容longa1[10][10][10];longa2[][10][10];longa3[][][10];voidf(longa4[][10][10]){a1[2][2][2]=a4[2][2][2];}main(){f(a1);}–a4和a2的类型描述一样，为什么对a4没有警告？实参表达式a1的类型是1010的长整型数组指针形参a4元素的类型与其一致，因此无类型错误形参数组的大小不重要，因实际操作实参数组了解类型系统的重要性•例3（C语言类型系统不足的例子）typedefstruct{intn;floata[];}record;recordp={2,{1.0,2.0}},q={3,{1.0,2.0,3.0}};main(){p=q;printf(“%d,%f,%f,%f\n”,p.n,p.a[0],p.a[1],p.a[2]);printf(“%d,%f,%f,%f\n”,q.n,q.a[0],q.a[1],q.a[2]);}经GCC:Ubuntu/Linaro4.6.31ubuntu5)4.6.3编译运行结果如下：3,1.000000,2.000000,3.0000001077936128,1.000000,2.000000,3.000000问题：q.n为什么被破坏了？了解类型系统的重要性•例3（C语言类型系统不足的例子）typedefstruct{intn;floata[];}record;recordp={2,{1.0,2.0}},q={3,{1.0,2.0,3.0}};main(){p=q;printf(“%d,%f,%f,%f\n”,p.n,p.a[0],p.a[1],p.a[2]);printf(“%d,%f,%f,%f\n”,q.n,q.a[0],q.a[1],q.a[2]);}赋值前：赋值后：21.02.031.02.03.031.02.03.01.02.03.0pqqp基本知识•类型系统–语言的组成部分，它由一组定型规则(typingrule)构成，这组规则用来给各种程序构造指派类型–设计类型系统的根本目的是用类型检查的方式来保证合法程序运行时侯的行为是良好的–类型系统的形式化类型表达式、定型断言、定型规则–类型检查算法期望静态完成类型检查。类型系统设计的一个重要设计目标是存在有效的静态类型检查算法基本知识•类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统-自然数表达式（需要定义它的语法）a+b,3-良形公式（逻辑断言，需要定义它的语法）a+b=3,(d=3)(c10)-推理规则abbcac基本知识•类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式a+b,3int,intint,pointer(int)-良形公式(也需要定义它的语法)a+b=3,(d=3)(c10)-推理规则abbcac基本知识•类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式a+b,3int,intint,pointer(int)-良形公式定型断言a+b=3,(d=3)(c10)x:int|–x+3:int-推理规则(|–左边部分x:int称为定型环境)(也需要定义它的语法)abbcac基本知识•类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式a+b,3int,intint,pointer(int)-良形公式定型断言a+b=3,(d=3)(c10)x:int|–x+3:int-推理规则定型规则|–M:int|–N:int|–M+N:intabbcac基本知识•定型规则的例子(ExpIndex)(0E2.valN1)(ExpDeref)(ExpFunCall)这些规则的特点：都是依据子结构的类型来确定一个结构的类型，易于类型检查的实现|E1:array(N,T),|E2:int|E1[E2]:T|E:pointer(T)|*E:T|E1:T1T2,|E2:T1|E1(E2):T2基本知识•举例说明类型系统带来的不便#definelength100typedeflongarray[length];longsum(arrayb){longs=0,i;for(i=0;ilength;i++){s=s+b[i];}}难以为char、short、int、long，甚至float和double类型的数组写一个通用的sum函数若使用inta[length]作为实参，编译器会报告类型错误多态类型•多态函数–普通的函数要求变元有唯一的类型，即函数体中的语句只能在变元类型固定的情况下执行–多态函数是指允许变元可以有不同类型的函数即函数体中的语句适用于不同的调用有不同变元类型的情况–C不支持多态函数–但有多态的算符，例如：关于取地址运算&的论述是：如果运算对象的类型是“…”，那么结果类型是指向“…”的指针任何类型都可以代替“…”多态类型•类型变量–排序函数：希望能应用于许多不同类型的数据–若用类型变量代表数组元素的类型，则排序函数的类型表达式是sort:(bool)array(…,)array(…,)其中bool是类型上的关系运算函数–进一步引入全称约束来表达多态函数的通用性sort:.(bool)array(…,)array(…,)&:.pointer()（取地址多态算符）[]:.array(…,)int(下标索引多态算符)多态类型•多态类型–多态函数和多态算符的类型–多态类型的成员可应用于多种类型的元素而不必提及这些类型sort:.(bool)array(…,)array(…,)&:.pointer()（取地址多态算符）[]:.array(…,)int(下标索引多态算符)多态类型•多态函数的类型推断–用简单的例子（取指针指向的对象）展示longderef(long*p){return*p}为适应可用于任何指针类型的变元，改成如下形参和结果类型都省略的函数deref(p){return*p}类型推断规则较为复杂，在此不介绍多态类型•多态函数定义的类型推断–根据函数体中的语句来推断多态函数的类型deref(p){//p的类型一无所知，暂定位p:return*p//需要根据*的类型来计算}由编程语言知，*:.pointer()对*的上述出现，脱掉，用新类型变量，得pointer()，再对和pointer()进行合一计算得=pointer()，即deref:pointer()再戴上，得deref:.pointer()多态类型