Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

TL;DR

This paper develops a phase-sensitive, proof-relevant parametricity framework for program modules using modal type theory, simplifying type abstraction and enabling new logical relations that distinguish between syntax and semantics.

Contribution

It introduces a synthetic, modal type-theoretic approach to program modules with proof-relevant parametricity, generalizing Reynolds' abstraction theorem to phase-sensitive, proof-relevant logical relations.

Findings

A proof-relevant, phase-sensitive generalization of Reynolds' abstraction theorem.

A new modal, synthetic account of phase distinction in parametricity.

Construction of simulations using representation invariants in a proof-relevant setting.

Abstract

The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh "synthetic" take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects. Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs -- simplifying the metatheory of strong sums over the collection of types, for although there can be no "relation classifying relations", one easily accommodates a "family classifying small families". Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan "logical relations as types", iterating our modal account of the phase distinction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.