Exploring the limitations of Contextual Modal Type Theory for Multi-Stage Programming
POPL SRC, 2024, with Jeremy Yallop, Alan Mycroft.
We present an initial exploration of the expressiveness gap between two well-known MSP paradigms, \(\lambda^\bigcirc\) and (simply-typed) CMTT. Murase et al., in 2023, present a very powerful extension to simply-typed CMTT based on first class contexts, which allows us to embed \(\lambda^\bigcirc\). We conjecture that this extension is overly powerful. To explore whether first class contexts are necessary, we create Lys, a language with both CMTT and OCaml’s features, and compare it with MetaOCaml (OCaml extended with \(\lambda^\bigcirc\)’s metaprogramming abilities), and attempt to translate MetaOCaml programs into Lys. Our preliminary results seem to suggest that first class contexts are only necessary to express MetaOCaml programs with type level abstractions. Nevertheless, it is still unclear whether a \(\lambda^\bigcirc\) only program still requires the expressivity of first class contexts.