Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Layered Modal ML: Syntax and Full Abstraction

Haoxuan Yin, Andrzej S. Murawski, C. -H. Luke Ong

TL;DR

This work introduces Layered Modal ML (LMML), a metaprogramming language that safely stores and executes open code by using contextual modal types to track free variables. It provides a two-layer Box/Letbox system, along with a two-layer type-depth mechanism, enabling strong type safety for higher-order references and open code. A semantic trace model based on operational game semantics establishes full abstraction for an imperative MetaML-like language, with CIU- and definability-based proofs linking contextual equivalence to trace inclusion. The result is a conservative extension of prior functional models to imperative metaprogramming, supported by rigorous preservation, progress, and safety proofs and illustrated by staging and code-duplication examples. The framework lays groundwork for enriching the language with more layers and broader typing contexts while maintaining robust safety and semantic adequacy.

Abstract

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Layered Modal ML (LMML), \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for LMML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

Layered Modal ML: Syntax and Full Abstraction

TL;DR

This work introduces Layered Modal ML (LMML), a metaprogramming language that safely stores and executes open code by using contextual modal types to track free variables. It provides a two-layer Box/Letbox system, along with a two-layer type-depth mechanism, enabling strong type safety for higher-order references and open code. A semantic trace model based on operational game semantics establishes full abstraction for an imperative MetaML-like language, with CIU- and definability-based proofs linking contextual equivalence to trace inclusion. The result is a conservative extension of prior functional models to imperative metaprogramming, supported by rigorous preservation, progress, and safety proofs and illustrated by staging and code-duplication examples. The framework lays groundwork for enriching the language with more layers and broader typing contexts while maintaining robust safety and semantic adequacy.

Abstract

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Layered Modal ML (LMML), \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for LMML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.
Paper Structure (30 sections, 38 theorems, 58 equations, 6 figures, 2 tables)

This paper contains 30 sections, 38 theorems, 58 equations, 6 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Type-safe metaprogramming with higher-order references for open code
  3. Closed instances of use with both call-by-name and call-by-value substitutions
  4. Operational game semantics for imperative metaprogramming
  5. Outline
  6. The language LMML
  7. Syntax
  8. Type System
  9. Operational Semantics
  10. Type Safety
  11. Closed Instances of Use
  12. Trace Model
  13. Names
  14. Value abstraction
  15. Actions
  16. ...and 15 more sections

Key Result

Theorem 1

If $\Sigma;\Psi;\Gamma\vdash_{i} M:T$, $\Sigma;\Psi;\Gamma\vdash_{} h:\mathbf{heap}$, and $(M,h)\rightarrow(M',h')$, then there exists $\Sigma'\supseteq\Sigma$ such that $\Sigma';\Psi;\Gamma\vdash_i M':T$, and $\Sigma';\Psi;\Gamma\vdash h':\mathbf{heap}$.

Figures (6)

  • Figure 1: Syntax
  • Figure 2: Well-formed types and typing contexts
  • Figure 3: Well-typed terms
  • Figure 4: Well-typed heaps, contexts and substitutions
  • Figure 5: Operational Semantics
  • ...and 1 more figures

Theorems & Definitions (88)

  • Theorem 1: Preservation
  • Lemma 1: Canonical forms
  • Theorem 2: Progress
  • Definition 1: Contextual preorder
  • Definition 2: Closed Instances of Use
  • Lemma 2: CIU Basics
  • Lemma 3: CIU Box
  • proof : Proof Sketch
  • Theorem 3: CIU
  • Definition 3: value abstraction
  • ...and 78 more