Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Three non-cubical applications of extension types

Tesla Zhang

TL;DR

This paper introduces a simple extension-type framework built around a universe of strict propositions $F$ and the syntax $\{A \mid \phi \\;▷\\; u\}$ to enable context-restricted typing. It develops the core typing rules and semantic intuition, then demonstrates three concrete PL applications: (i) controlling unfolding via per-definition propositions $\phi_f$ and the transitive propagation of unfolding; (ii) definitional projection for partially specified records using singletons and projective extension types; and (iii) opaque encodings for metaprogramming to simplify encodings while preserving the ability to reason about the original structure. The work also connects extension types to type theories with shapes, including cubical and simplicial variants, highlighting the expressiveness gained in metatheory, modularity, and practical type-system design. Overall, the framework provides a flexible, well-understood mechanism for controlling evaluation, enabling robust metaprogramming, and enriching the design space of dependent type theories with shapes.

Abstract

The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these applications, including on records, metaprogramming, controlling unfolding, and some more exotic ones.

Three non-cubical applications of extension types

TL;DR

This paper introduces a simple extension-type framework built around a universe of strict propositions and the syntax to enable context-restricted typing. It develops the core typing rules and semantic intuition, then demonstrates three concrete PL applications: (i) controlling unfolding via per-definition propositions and the transitive propagation of unfolding; (ii) definitional projection for partially specified records using singletons and projective extension types; and (iii) opaque encodings for metaprogramming to simplify encodings while preserving the ability to reason about the original structure. The work also connects extension types to type theories with shapes, including cubical and simplicial variants, highlighting the expressiveness gained in metatheory, modularity, and practical type-system design. Overall, the framework provides a flexible, well-understood mechanism for controlling evaluation, enabling robust metaprogramming, and enriching the design space of dependent type theories with shapes.

Abstract

The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these applications, including on records, metaprogramming, controlling unfolding, and some more exotic ones.
Paper Structure (13 sections, 10 equations, 1 figure)

This paper contains 13 sections, 10 equations, 1 figure.

Table of Contents

  1. Applications of extension types
  2. Controlling unfolding
  3. Partially applied records with definitional projection
  4. Opaque encoding for metaprogramming
  5. Introduction to extension types
  6. Context restrictions with propositions
  7. Extension types and their typing rules
  8. Extension types in action
  9. Controlling unfolding and metaprogramming
  10. Definitional projection with singletons
  11. Definitional projection with projective extension types
  12. Type theory with shapes
  13. Related Work

Figures (1)

  • Figure 2.1: Rules of extension types

Theorems & Definitions (10)

  • Remark 1.2
  • Remark 2.1: ST$λ$C
  • Remark 2.2
  • Remark 2.5: Semantics
  • Remark 2.7: Semantics
  • Remark 2.8
  • Remark 3.2
  • Remark 3.3
  • Remark 3.5
  • Remark 3.6