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

本文讨论了一种带约束的多态类型系统，引入了约束类型，约束与全称量化的结合使得参数化多态函数的应用更安全，同时也为重工的表示和实现提供了一个新的途径，提高了类型表示的抽象度。本文讨论的类型系统具有两个不同层次的类型结构，约束的引入与肖去是不同层次上的操作，最后，本文人出了类型检查算法Ｗｒ，并证明了此算法中约束的可满足性是可判定的。

A POLYMORPHIC TYPE SYSTEM WITH CONSTRAINTS

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.