Artículo
Type Soundness for Path Polymorphism
Fecha de publicación:
11/2016
Editorial:
Elsevier
Revista:
Electronic Notes in Theoretical Computer Science
ISSN:
1571-0661
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
Path polymorphism is the ability to define functions that can operate uniformly over arbitrary recursively specified data structures. Its essence is captured by patterns of the form xy which decompose a compound data structure into its parts. Typing these kinds of patterns is challenging since the type of a compound should determine the type of its components. We propose a static type system (i.e. no run-time analysis) for a pattern calculus that captures this feature. Our solution combines type application, constants as types, union types and recursive types. We address the fundamental properties of Subject Reduction and Progress that guarantee a well-behaved dynamics. Both these results rely crucially on a notion of pattern compatibility and also on a coinductive characterisation of subtyping.
Palabras clave:
PATH POLYMORPHISM
,
PATTERN MATCHING
,
STATIC TYPING
,
Λ-CALCULUS
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(SEDE CENTRAL)
Articulos de SEDE CENTRAL
Articulos de SEDE CENTRAL
Citación
Viso, Andrés Ezequiel; Bonelli, Eduardo Augusto; Ayala Rincón, Mauricio; Type Soundness for Path Polymorphism; Elsevier; Electronic Notes in Theoretical Computer Science; 323; 11-2016; 235-251
Compartir
Altmétricas