Typed path polymorphism.
Theoretical Computer Science(2019)
摘要
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.
更多查看译文
关键词
λ-calculus,Pattern matching,Path polymorphism,Static typing,Type checking
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要