Simplifying and solving qualified types for principal type specialisation
Material type:
ArticleSubject(s): Online resources: Summary: 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.
| Item type | Home library | Collection | Call number | URL | Status | Date due | Barcode | |
|---|---|---|---|---|---|---|---|---|
Capítulo de libro
|
Biblioteca de la Facultad de Informática | Biblioteca digital | A0101 (Browse shelf(Opens below)) | Link to resource | Recurso en Línea |
Browsing Biblioteca de la Facultad de Informática shelves, Collection: Biblioteca digital Close shelf browser (Hides shelf browser)
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.
Proceedings del Workshop Argentino de Informática Teórica (WAIT༿), dentro de las 32das Jornadas Argentinas de Informática e Research Operativa (JAIIO ༿), September 2003.