Post #1506853

@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