Contextual MetaML: Syntax and Full Abstraction

TL;DR

This paper introduces Contextual MetaML, a novel metaprogramming language that guarantees type safety for open code and provides a semantic model for program equivalence, including full abstraction.

Contribution

It is the first language supporting open code with strong type safety and a semantic model establishing full abstraction for imperative MetaML-style languages.

Findings

Supports storing and running open code with type safety

Provides a semantic model for contextual equivalence

Establishes full abstraction for an imperative MetaML-style language

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 Contextual MetaML, \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 Contextual MetaML, 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.