A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Andreas Abel, Nils Anders Danielsson and Oskar Eriksson
Proceedings of the ACM on Programming Languages, Volume 7, Issue ICFP, 2023 (ICFP 2023, 10.1145/3607862). [pdf, highlighted Agda code, zip file with code]

Abstract

We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Π-types, weak and strong Σ-types, natural numbers, an empty type, and a universe, and we also extend the theory with a unit type and graded Σ-types. The theory is parameterized by a modality, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable.

The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped λ-calculus and removes erasable content, in particular function arguments with the “erasable” grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak Σ-types.

Erratum

The discussed modalities for linear and/or affine types allow one to conclude that a certain doubling function, basically λ n. n + n, is linear/affine. One can also prove that, with the modalities for linear types, a certain (obvious) implementation of addition with a linear type is not well-resourced, even though that would arguably make sense.

The paper's main focus is not on linear or affine types, and the conclusions imply that there is no "serious soundness argument for linearity" in the paper. However, at least one claim might be incorrect.

On page 15 an informal argument leads to the conclusion that "There are thus three constraints that the context in the conclusion of the rule […] must satisfy", and these constraints are used to motivate the natrec-star operators. Furthermore the alternative usage rule for natrec in Section 7.1.4 is directly based on those three constraints: the constraints are required to hold, but otherwise there are no restrictions on the usage context in the conclusion. However, the problems mentioned above also affect the variant of the theory with this usage rule. In particular, the definition of addition with a linear type is not well-resourced for the linear types modality. Thus, if the three constraints must be satisfied, then this form of addition is not linear.

In preliminary work we have replaced the natrec-star operators with something more general. This makes it possible to have a linear types modality for which the "linear" doubling function is not well-resourced, and for which addition is linear. If this linear types modality can be shown to be "correct", then the claim on page 15 is in some sense incorrect.