Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming

Junyoung Jang, Brigitte Pientka

TL;DR

Elevator is described, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities that proves the substructurality of variable references and type safety of the language and establishes mode safety, which guarantees that the evaluation of a term does not access a value in an inaccessible memory.

Abstract

We describe Elevator, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities. In this setting, we distinguish between multiple memory regions using modes where each mode has a specific set of structural properties. This allows us not only to capture linear (i.e. garbage-free) memory regions and (ordinary) intuitionistic (i.e. garbage-collected or persistent) memory regions, but also to capture accessibility between the memory regions using a preorder between modes. This preorder gives us the power to describe monadic and comonadic programming. As a consequence, it extends the existing logical view of metaprogramming in two directions: first, it ensures that code generation can be done efficiently by controlling memory accesses; second, it allows us to provide resource guarantees about the generated code (i.e. code that is for example garbage-free). We present the static and dynamic semantics of Elevator. In particular, we prove the substructurality of variable references and type safety of the language. We also establish mode safety, which guarantees that the evaluation of a term does not access a value in an inaccessible memory.

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming

TL;DR

Elevator is described, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities that proves the substructurality of variable references and type safety of the language and establishes mode safety, which guarantees that the evaluation of a term does not access a value in an inaccessible memory.

Abstract

We describe Elevator, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities. In this setting, we distinguish between multiple memory regions using modes where each mode has a specific set of structural properties. This allows us not only to capture linear (i.e. garbage-free) memory regions and (ordinary) intuitionistic (i.e. garbage-collected or persistent) memory regions, but also to capture accessibility between the memory regions using a preorder between modes. This preorder gives us the power to describe monadic and comonadic programming. As a consequence, it extends the existing logical view of metaprogramming in two directions: first, it ensures that code generation can be done efficiently by controlling memory accesses; second, it allows us to provide resource guarantees about the generated code (i.e. code that is for example garbage-free). We present the static and dynamic semantics of Elevator. In particular, we prove the substructurality of variable references and type safety of the language. We also establish mode safety, which guarantees that the evaluation of a term does not access a value in an inaccessible memory.

Paper Structure

This paper contains 27 sections, 11 theorems, 29 equations, 9 figures.

Table of Contents

  1. Introduction
  2. 1. Contextualizing Adjoint Logic
  3. 2. An Operational Semantics for Adjoint Modalities Suitable for Metaprogramming
  4. 3. Adjoint Modalities and System-F style Polymorphism
  5. Motivations
  6. Code Generation Using Contextual Adjoint Modalities
  7. Polymorphic Code Generation and Cross-Stage Persistent Type Variables
  8. Enforcing linearity
  9. Generating code with resource guarantees
  10. Elevator: Polymorphic Metaprogramming Using Adjoint Modalities
  11. Mode Specification
  12. Syntax
  13. Context Operations
  14. Substitution
  15. Type System and Substructurality
  16. ...and 12 more sections

Key Result

lemma 1

Figures (9)

  • Figure 1: Well-Formedness of Kinds, Types, and Contexts
  • Figure 2: Typing Rules for Terms and Substitutions
  • Figure 3: Syntax of weak normal/neutral forms and normal templates in mode $k$
  • Figure 4: Small-step semantics of Elevator
  • Figure 5: Equivalence over mode $n$ on contexts
  • ...and 4 more figures

Theorems & Definitions (11)

  • lemma 1: Properties of Context Split
  • theorem 1: Termination of Substitution
  • lemma 2: Properties of Substitution Split
  • theorem 2: Substructurality of Variable References
  • lemma 3: Splitting
  • lemma 4: Effect of Splitting
  • lemma 5: Substitution Lemma
  • theorem 3: Preservation
  • theorem 4: Progress
  • lemma 6: Diamond Modulo Equivalence Over a Mode
  • ...and 1 more