摘要
本文讨论了一种带约束的多态类型系统，引入了约束类型．约束与全称量化的结合使得参数化多态函数的应用更安全，同时也为重载的表示和实现提供了一个新的途径，提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构，约束的引入与消去是不同层次上的操作．最后，本文绘出了类型检查算法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.
出处
《计算机学报》
EI
CSCD
北大核心
1999年第4期343-350,共8页
Chinese Journal of Computers
