Simplifying and solving qualified types for principal type specialisation
Martínez López, Pablo Ernesto
Simplifying and solving qualified types for principal type specialisation
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 06/03/2009)
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.
DIF-M2602
PROGRAMACIÓN AUTOMÁTICA
PROGRAMACIÓN FUNCIONAL
LENGUAJES DE PROGRAMACIÓN
Simplifying and solving qualified types for principal type specialisation
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 06/03/2009)
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.
DIF-M2602
PROGRAMACIÓN AUTOMÁTICA
PROGRAMACIÓN FUNCIONAL
LENGUAJES DE PROGRAMACIÓN