Type soundness for path polymorphism

DOI10.1016/J.ENTCS.2016.06.015MaRDI QIDQ1744425zbMATH OpenOpenAlexWikidataFDO

Authors Andrés Viso, Eduardo Bonelli, Mauricio Ayala-Rincón

Publication date 23 April 2018

Full work available at URL https://arxiv.org/abs/1601.03271

zbMATH Keywords

pattern matching\(\lambda\)-calculusstatic typingpath polymorphism

Mathematics Subject Classification ID

Data structures (68P05) Functional programming and lambda calculus (68N18)

Abstract: 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 $x,y$ 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.

Recommendations

• Typed path polymorphism
• Efficient type checking for path polymorphism
• Polymorphic type inference and containment
• Polymorphic typed defunctionalization
• Interaction between path and type constraints
• Polymorphic typed defunctionalization and concretization
• Type inference for polymorphic references
• Type inference in polymorphic type discipline
• scientific article; zbMATH DE number 7577586
• A sound polymorphic type system for a dialect of \(C\)

Cites work

• scientific article; zbMATH DE number 1701351 (Why is no real title available?)
• scientific article; zbMATH DE number 1722700 (Why is no real title available?)
• scientific article; zbMATH DE number 1183236 (Why is no real title available?)
• scientific article; zbMATH DE number 2087431 (Why is no real title available?)
• scientific article; zbMATH DE number 919844 (Why is no real title available?)
• An extension of system \(F\) with subtyping
• Computer Science Logic
• Efficient and flexible matching of recursive types
• Efficient recursive subtyping
• First-class patterns
• Pattern Calculus
• Programming Languages and Systems
• Pure patterns type systems
• Rewriting calculus with(out) types
• Semantics of typed lambda-calculus with constructors
• Subtyping recursion and parametric polymorphism in kernel Fun
• The polymorphic rewriting-calculus [type checking vs. type inference]
• The rewriting calculus. II
• The λ-calculus with constructors: Syntax, confluence and separation
• Type soundness for path polymorphism
• Typed Lambda Calculi and Applications
• Types and programing languages
• Types for Proofs and Programs

Cited in

(6)

• Type soundness proofs with definitional interpreters
• Type soundness for path polymorphism
• Efficient type checking for path polymorphism
• Typed path polymorphism
• Polymorphic regular tree types and patterns
• Pure pattern calculus à la de Bruijn

This page was built for publication: Type soundness for path polymorphism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1744425)