Typed path polymorphism

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.