Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Graded Modal Dependent Type Theory with Erasure, Formalized

Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

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 weak and strong unit types and graded $Σ$-types. The theory is parameterized by a modality structure, 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.

A Graded Modal Dependent Type Theory with Erasure, Formalized

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 weak and strong unit types and graded -types. The theory is parameterized by a modality structure, 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.

Paper Structure

This paper contains 23 sections, 19 theorems, 11 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Relation to the state of the art
  3. Form of judgement: separate and one-sided sage accounting
  4. Usage accounting also in types
  5. Semantics refines resource-free semantics
  6. Formalization
  7. Universes and large eliminations
  8. Instance: erasure, justified by a logical relation
  9. Modalities organized as ordered semirings
  10. Type theory with grades
  11. Syntax
  12. Weakening and substitution
  13. Typing and equality
  14. Reduction
  15. Assigning grades
  16. ...and 8 more sections

Key Result

Theorem 4.1

If $\Gamma \vdash{} t \longrightarrow^* u \mathrel{:} A$ with $t$ in WHNF, then $t = u$. Similarly, if $\Gamma \vdash{} A \longrightarrow^* B$ with $A$ in WHNF, then $A = B$.

Figures (13)

  • Figure 1: Operator definitions for some modality structures.
  • Figure 2: Well-formed contexts, \thmBaseLink/Definition.Typed.html#%E2%8A%A2_, types, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_, variables, \thmBaseLink/Definition.Typed.html#_%E2%88%B7_%E2%88%88_, and terms, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%88%B7_.
  • Figure 3: Equality of types, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%89%A1_, and terms, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%89%A1_%E2%88%B7_.
  • Figure 4: Weak head reduction of types, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%87%92_, and terms, \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%87%92_%E2%88%B7_, as well as their reflexive, transitive closures \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%87%92%2A_ and \thmBaseLink/Definition.Typed.html#_%E2%8A%A2_%E2%87%92%2A_%E2%88%B7_.
  • Figure 5: The grade assignment relation \thmBaseLink/Graded.Usage.html#_%E2%96%B8%5B_%5D_.
  • ...and 8 more figures

Theorems & Definitions (45)

  • Definition 3.1: Modality structure
  • Remark 1: Atkey's Dependent Tensor Product Types
  • Remark 2: Eliminator for $\Sigma_{\&}$, Projections for $\Sigma_{\otimes}$
  • Theorem 4.1: whnfs do not reduce
  • Theorem 4.2: whnf is unique
  • Definition 5.1: Usage relation
  • Definition 5.2: Usage inference
  • Theorem 5.1: Principality
  • proof
  • Theorem 5.2: Decidability
  • ...and 35 more