Post #1125810

Replies (2)

• @cbaberle@mathstodon.xyz 2025-03-06 16:47

  **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.

  Open ##1506845

• @bentnib@types.pl 2025-03-07 14:22

  @cbaberle @chrisamaphone Nicely written! I've not seen anyone explore the ordered case before. There's also Linear Plotkin-Abadi logic ( https://arxiv.org/abs/cs/0611004 ) that axiomatises parametricity reasoning for a linear type system. Their motivation was to use linear types as an abstract domain theory though. I did a short example of linear types + logical relations to prove that linear functions from lists to lists are always permutations: https://github.com/bobatkey/sorting-types/blob/master/agda/Linear.agda . The original idea for this was from @pigworker The was later (briefly) written up in a more general form for any semiring-graded system by @mudri and me: https://bentnib.org/context-constrained.pdf and also in a slightly different way by Bernardy and Abel: https://dl.acm.org/doi/10.1145/3408972

  Open ##1506853