一种带约束的多态类型系统  

A POLYMORPHIC TYPE SYSTEM WITH CONSTRAINTS

作　　者：郑红军[1] 张乃孝[1] 

机构地区：[1]北京大学数学学院信息科学系,北京100871

出　　处：《计算机学报》1999年第4期343-350,共8页Chinese Journal of Computers

摘　　要：本文讨论了一种带约束的多态类型系统，引入了约束类型．约束与全称量化的结合使得参数化多态函数的应用更安全，同时也为重载的表示和实现提供了一个新的途径，提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构，约束的引入与消去是不同层次上的操作．最后，本文绘出了类型检查算法Wτ，并证明了此算法中约束的可满足性是可判定的．This paper concentrates on a polymorphic type system with constraints based on constrained types. By Incorporating constraints into universal quantification, the system can make applications of parametrically polymorphic function more safe. The constrained types provide a new way for expressing and implementing overloading. The Incorporating can improve the expressiveness of types. There are two layers with different type structures in the type system given in this paper. Introduction and elimination of constraints are in the different levels. It is proved that the satisfiability of constraints in W, which is a type checking algorithm proposed in the paper,is decidable.

关 键 词：约束类型 类型检查 多态类型系统 程序设计语言 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]