Type Soundness for Path Polymorphism

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 t...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Viso, A., Bonelli, E., Ayala-Rincón, M.
Formato: JOUR
Materias:
Path Polymorphism
Pattern Matching
Static Typing
λ-Calculus
Data structures
Differentiation (calculus)
Pattern matching
Compound data structure
Fundamental properties
Pattern calculus
Recursive types
Run-time analysis
Static type systems
Static typing
Subject reduction
Calculations
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_15710661_v323_n_p235_Viso
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_15710661_v323_n_p235_Viso
record_format dspace
spelling todo:paper_15710661_v323_n_p235_Viso2023-10-03T16:27:12Z Type Soundness for Path Polymorphism Viso, A. Bonelli, E. Ayala-Rincón, M. Path Polymorphism Pattern Matching Static Typing λ-Calculus Data structures Differentiation (calculus) Pattern matching Compound data structure Fundamental properties Pattern calculus Recursive types Run-time analysis Static type systems Static typing Subject reduction Calculations 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. © 2016 The Author(s) Fil:Bonelli, E. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_15710661_v323_n_p235_Viso
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Path Polymorphism
Pattern Matching
Static Typing
λ-Calculus
Data structures
Differentiation (calculus)
Pattern matching
Compound data structure
Fundamental properties
Pattern calculus
Recursive types
Run-time analysis
Static type systems
Static typing
Subject reduction
Calculations
spellingShingle Path Polymorphism
Pattern Matching
Static Typing
λ-Calculus
Data structures
Differentiation (calculus)
Pattern matching
Compound data structure
Fundamental properties
Pattern calculus
Recursive types
Run-time analysis
Static type systems
Static typing
Subject reduction
Calculations
Viso, A.
Bonelli, E.
Ayala-Rincón, M.
Type Soundness for Path Polymorphism
topic_facet Path Polymorphism
Pattern Matching
Static Typing
λ-Calculus
Data structures
Differentiation (calculus)
Pattern matching
Compound data structure
Fundamental properties
Pattern calculus
Recursive types
Run-time analysis
Static type systems
Static typing
Subject reduction
Calculations
description 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. © 2016 The Author(s)
format JOUR
author Viso, A.
Bonelli, E.
Ayala-Rincón, M.
author_facet Viso, A.
Bonelli, E.
Ayala-Rincón, M.
author_sort Viso, A.
title Type Soundness for Path Polymorphism
title_short Type Soundness for Path Polymorphism
title_full Type Soundness for Path Polymorphism
title_fullStr Type Soundness for Path Polymorphism
title_full_unstemmed Type Soundness for Path Polymorphism
title_sort type soundness for path polymorphism
url http://hdl.handle.net/20.500.12110/paper_15710661_v323_n_p235_Viso
work_keys_str_mv AT visoa typesoundnessforpathpolymorphism
AT bonellie typesoundnessforpathpolymorphism
AT ayalarinconm typesoundnessforpathpolymorphism
_version_ 1782030053266161664

Ejemplares similares