Multi-stage programming is a long-standing paradigm used for systematically reconciling abstraction and performance via runtime code generation. Two lines of research have emerged. One approach, based on linear temporal types (e.g. MetaOCaml), enables compositional symbolic evaluation but fails to enable safe code execution and interacts poorly with effects. The other approach, based on a contextual relaxation of modal S4 types (CMTT), does not present these problems but is known to be less expressive.

This work wants to build on the numerous theoretical works on CMTT attempting to close this gap. More specifically, we harness the insights of Jang et al. with system F polymorphism — a significant boost in expressiveness; and those of Murase et al. with contextual polymorphism — significantly narrowing, if not closing the gap with temporal types. We aim to address some of the questions they leave open: what is the relationship between these two calculi? Is contextual polymorphism necessary to bridge the gap, and is it sufficient to express more practical MetaOCaml applications?

In this work, we explore these questions with a practical perspective. We implement Lys, a language based on a subset of Jang et al.‘s calculus, and use it to attempt to reimplement MetaOCaml applications — a stream fusion library, and a tagless final interpreter. This enables us to shed light on the relationship between System F CMTT and contextual polymorphic CMTT. We provide empirical evidence that System F alone fails to reach the expressiveness of MetaOCaml and that general first-class contexts are needed for practical applications. We also find that System F polymorphism can, in some cases, simulate context polymorphism, with the caveat of additional runtime overhead. We leave further exploration based on these insights to future work.