Moebius：Metaprogramming using Contextual Types -- The stage where System F can pattern match on itself（Moebius：Metaprogramming using Contextual Types）
Moebius: Metaprogramming using Contextual Types -- The stage where System F can pattern match on itself (Long Version)
摘要：
我们描述的元编程语言，Moebius，它支持生成多态代码，更重要的是通过模式匹配多态代码的分析的基础。Moebius有两个主要成分：1）我们利用上下文模态类型来描述开放代码以及它有意义的上下文。在Moebius中，开放代码可以依赖于类型和术语变量（级别0），其值在稍后阶段提供，以及代码变量（级别1），代表在稍后阶段提供的代码模板。这就产生了一个多层次的模态演算，它支持System-F风格的多态性，并形成了多态代码生成的基础。2)我们扩展了多级模态模式演算以支持代码上的模式匹配。由于多态代码上的模式匹配可以细化多态类型变量，因此我们扩展了类型理论基础，以生成和跟踪出现的类型约束。我们还给出了一个操作语义并证明了类型保持性。我们的Moebius多层次模态基础为开放代码的生成和模式匹配提供了适当的抽象，而无需提交变量绑定和上下文的具体表示。因此，我们的工作是一个步骤，建立一个通用的类型理论的基础，多阶段的元编程，一方面，强制执行强类型保证，另一方面，使其易于生成和操作代码。这将使我们能够充分利用元编程的潜力，而不会牺牲我们正在生产和运行的代码的可靠性和信任。
英文摘要：
We describe the foundation of the metaprogramming language, Moebius, which supports the generation of polymorphic code and, more importantly the analysis of polymorphic code via pattern matching. Moebius has two main ingredients: 1) we exploit contextual modal types to describe open code together with the context in which it is meaningful. In Moebius, open code can depend on type and term variables (level 0) whose values are supplied at a later stage, as well as code variables (level 1) that stand for code templates supplied at a later stage. This leads to a multi-level modal lambda-calculus that supports System-F style polymorphism and forms the basis for polymorphic code generation. 2) we extend the multi-level modal lambda-calculus to support pattern matching on code. As pattern matching on polymorphic code may refine polymorphic type variables, we extend our type-theoretic foundation to generate and track typing constraints that arise. We also give an operational semantics and prove type preservation. Our multi-level modal foundation for Moebius provides the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Hence, our work is a step towards building a general type-theoretic foundation for multi-staged metaprogramming that, on the one hand, enforces strong type guarantees and, on the other hand, makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing the reliability of and trust in the code we are producing and running.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
