Research indexJournal article
Substructural Parametricity
Aberlé, Crary, Martens and 1 other
DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)1 Jan 2025Open access
NobleIDark:/48914/w1/20261005/5FB28958DOI10.4230/lipics.fscd.2025.4
Substructural Parametricity
Aberlé, Crary, Martens and 1 other · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2025
NobleIDark:/48914/w1/20261005/5FB28958DOI10.4230/lipics.fscd.2025.4
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.