Formalization of Opaque Definitions for a Dependent Type Theory

Abstract

Definitions allow for the efficient reuse of code, but the process of unfolding complex nested definitions may cause usability issues for the programmer. Opaque definitions help mitigate this by restricting the unfolding of definitions at type-checking time, but their implementation demands some subtlety—for instance, subject reduction may be lost if an opaque type definition doesn’t unfold in exactly the right way. Despite this, there has been relatively little work on formally characterizing opaque definitions. We contribute here a formalization of opaque top-level definitions based on their implementation in the Agda programming language. The formalization is fully mechanized in Agda as an extension of the prior graded-type-theory project. We give typing and reduction rules for the definitions, then show, through a Kripke logical relation argument, that they enjoy many of the usual desirable type-theoretic properties: subject reduction, normalization, consistency, decidability of conversion, and so on.