Abstract Effects and Proof-Relevant Logical Relations

TL;DR

This paper introduces proof-relevant logical relations using setoids to address issues in traditional Kripke logical relations, enabling more accurate semantic reasoning and validation of program equivalences involving effects.

Contribution

It presents a novel proof-relevant logical relation framework with setoids, solving admissibility and dependency issues in traditional models, and demonstrates applications in program equivalence and effect systems.

Findings

Addresses admissibility issues in logical relations

Enables validation of more effect-based program equivalences

Provides a denotational semantics for region-based effect systems

Abstract

We introduce 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. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves two well-known problems caused by the use of existential quantification over future worlds in traditional Kripke logical relations: 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.