Substructural Parametricity
C. B. Aberlé, Chris Martens, Frank Pfenning
TL;DR
The paper addresses how parametricity interacts with substructural type systems to yield precise, type-level properties. It develops unary logical relations parameterized by a resource algebra $M$ (with operation $\cdot$ and unit $\epsilon$) and specializes them to monoid-based interpretations for ordered types and commutative-monoid interpretations for linear types, proving a fundamental theorem of logical predicates. This framework derives extensional inhabitancy results, such as the unique inhabitants of polymorphic list operators and certain tree traversals, and a striking result that the ordered type of list fold is inhabited only by the fold function. The work provides a principled method to reason about substructural parametricity and suggests future extensions to adjoint frameworks for combining modes, all within a closed-term logical-relations approach that simplifies initial proofs while enabling rich semantic conclusions.
Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.