Martin Hofmann, Proof-relevant logical relations
Proof-relevant logical relations
(joint work with Nick Benton, Andrew Kennedy, Vivek Nigam)
We explore a novel variant of logical relations that maps types not merely to partial equivalence relations on values as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. A setoid is like a category all of whose morphisms are isomorphisms (a groupoid) with the exception that no equations between these morphisms are required to hold. We interpret the objects of a setoid as establishing the semantic well-formedness (type inhabitation) of values, whilst its morphisms are understood as proofs of semantic equivalence.
The transition to proof-relevance allows one to remedy the notorious problems brought about by the use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.
We illustrate the novel format with two applications: a direct-style validation of Pitts and Stark's equivalences for ``new'' and a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked; non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module soundly to validate more effect-based program equivalences than would be possible with traditional effect systems.