WG211/M26Kovacs

Thinning-stable metaprogramming

András Kovács

In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of such type can inspect Γ in arbitrary unhygienic ways. So we'd like to restrict ourselves to metaprograms that are stable under certain morphisms between object-level scopes. Previous works have explored stability under a) substitution b) variable renaming c) injective variable renaming, in various logical frameworks and nominal and staged calculi. I investigate stability under thinning (also known as order-preserving embedding).