Internalizing Extensions in Lattices of Type Theories

TL;DR

This paper investigates embedding extension tracking directly into the type system of lattices of type theories using DCOI, aiming for more precise dependency specifications and improved reuse of definitions.

Contribution

It proposes using the Dependent Calculus of Indistinguishability (DCOI) to internalize extension tracking within the type system, enhancing precision and consistency management.

Findings

DCOI can model extension dependencies as a lattice of dependency levels.

Internalizing extension tracking enables more precise specifications.

Potential for improved reuse and consistency in proof assistants.

Abstract

Many proof assistants allow the use of features and axioms that increase their expressive power. However, these extensions must be used with care, as some combinations are known to lead to logical inconsistencies. Therefore, proof assistants include mechanisms that track which extensions are used in a proof development or module, ensuring that incompatible extensions are not used simultaneously. Unfortunately, existing extension tracking mechanisms are external to the type system. This means that we cannot specify precisely which extensions a definition depends on. Having the ability to write more precise specifications means we are not picking an overapproximation of the extensions needed, which prevents reusing definitions in the presence of incompatible extensions. Furthermore, we cannot refer to definitions that use incompatible extensions even if they are never used in inconsistent ways. The reasoning principles of one extension therefore cannot be used as a metatheory to reason about the properties of an incompatible extension. In this report, I explore the use of the Dependent Calculus of Indistinguishability (DCOI) by Liu et al. for extension tracking. DCOI is a dependent type system with dependency tracking, where terms and variables are assigned dependency levels alongside their types. These dependency levels form a lattice that describes which levels are permitted to access what. To instead track extensions, each set of extensions would correspond to a dependency level, and the lattice would describe how extensions are permitted to interact.