Type Soundness for Path Polymorphism

TL;DR

This paper introduces a static type system for path polymorphism, enabling safe and uniform manipulation of complex recursive data structures through pattern matching, ensuring soundness and well-behaved program dynamics.

Contribution

It presents a novel type system combining type application, constants, union, and recursive types to handle path polymorphism without runtime analysis.

Findings

Proves Subject Reduction and Progress for the type system

Defines a notion of pattern compatibility

Uses coinductive subtyping characterization

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.