Typed path polymorphism

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

Research output: Contribution to journalArticlepeer-review


Path polymorphism enables the definition of functions uniformly applicable to arbitrary recursively specified data structures. Path polymorphic function declarations rely on patterns of the form x y (i.e. the application of two variables), which decompose a data structure into its parts. We propose a static type system for a calculus that captures this feature, combining constants as types, union types and recursive types. The fundamental properties of Subject Reduction and Progress are addressed to guarantee well-behaved dynamics; they rely crucially on a novel notion of pattern compatibility. We also introduce an efficient type-checking algorithm by formulating a syntax-directed variant of the type system. This involves algorithms for checking type equivalence and subtyping, both based on coinductive characterizations of those relations.

Original languageEnglish
Pages (from-to)111-130
Number of pages20
JournalTheoretical Computer Science
StatePublished - Aug 16 2019

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


  • Path polymorphism
  • Pattern matching
  • Static typing
  • Type checking
  • λ-calculus


Dive into the research topics of 'Typed path polymorphism'. Together they form a unique fingerprint.

Cite this