Moebius: Metaprogramming using Contextual Types
summary
Moebius provides a formal metaprogramming core: a multi-level contextual modal lambda-calculus that generates System F–style polymorphic code, lets open code depend on both term/type variables and higher-level code templates, and supports pattern matching on polymorphic code. The system emits and tracks typing constraints when patterns refine type variables, gives operational semantics, and proves type preservation. Examples show reduced redundant staging redexes and direct code-template substitution; implementation and optimizer work remain future steps.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:13Tension between features and typesafeties
- 2:05Overview
- 2:51Contextual Model
- 3:42Calculus
- 5:01Code fragment
- 7:26Code template
- 9:44Local context
- 15:17Type Refinement
- 19:52Questions
related talks
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
19mExtensible Metatheory Mechanization via Family Polymorphism
45mLogic Meta Programming for Functional Languages
50mA Type-Theoretic Framework for Certified Meta-programming
36mDependently Typed Multi-Stage Programming, Revisited
24mLocal Contextual Type Inference
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
59mMeta++: Language Support for Advanced Generative Programming