Simplifying and solving qualified types for principal type specification

Abstract. Principal Type Specialisation is an approach to Type Specialisation designed to generate polymorphic residual programs and giving chance of modular specialisation. Principality is obtained by using a system of qualified types (types enriched with predicates, or constraints) to defer some decisions until link-time, when information from the whole program has been gathered. In order to complete specialisations, it is necessary to provide “solutions” for the predicates, together with evidence that they hold. In this paper we address the problem of simplifying and solving predicates produced by principal type specialisation. We give a formalization of the simplification and solving problems. The simplification process (essentially the task of removing redundant predicates) generates substitutions and conversions as tools for soundly modifying terms and types accordingly. We study the basic properties of simplifications in an abstract way, and implement one simplification relation. The process of solving predicates is then defined in terms of simplification and both notions are incorporated to the specialisation process.