A rewrite-based type discipline for a subset of computer algebra (Q1176783)

This paper is originated from computer algebra and its main features are the use of terms of an order-sorted algebra to denote polymorphic types with properties and the use of rewrite rules to define subtyping relations. The type system aims at the contradictory goals which must be solved simultaneously: static type checking and the possibility to omit typing information. A solution is to use a type inference algorithm, which allows the system to compute statically the type of every expression with no typing information provided by the user. A basic idea to handle polymorphism is to denote types by terms where a given set of functors denotes the construction of more complex types from simpler ones and where variables ranges over types. A type system into which polymorphism with properties may be expressed, and where subtyping information is given through rewrite rules is presented. This system uses an initial term algebra and a presentation (an order sorted signature and a finite set of subtype rules \(l_ i-r_ i\)). The rules contained in a presentation are used to derive types by ``rewriting''. In this system, unfortunately, the type inference problem is undecidable, but the authors show that when some not unreasonable restrictions are made it is possible to get an efficient semi-decision procedure. Many relations with other work are presented.