Class-Sort polymorphism in GLIDER

Abstract

In this paper we propose a semantic framework for dealing with class-sort polymorphism as presented in the last version of GLIDER. This kind of polymorphism is quite more powerful than the standard sort polymorphism that can be found in a number of functional languages (e.g. Standard ML, Miranda, etc.).In particular, polymorphic or generic types are considered to be parameterized by specifications (i.e. sorts, operations and even axioms) and not just by sorts. The semantic framework defined is based on the idea that the type structure underlying a certain specification should be a category. In particular, this category has, as objects, the given specifications including all the implicit instances of the generic types and the derived subclass relationships. Then, the semantics of a GLIDER specification is a category having the "same structure" as the underlying category of types.