Type-Directed Macros: A New Frontier in Programming Language Design

Macros have long been a powerful tool in programming languages, allowing developers to extend syntax and automate repetitive code generation. Traditional macros, like those in Lisp or C, operate purely at the syntactic level: they transform code before any type information is known. While this makes them flexible, it also limits their ability to write abstractions that adapt based on types.

Enter type-directed macros — a next-generation approach that brings type information into the macro expansion phase. By letting macros “see” and specialize based on the types of expressions, we can write far more powerful and safe abstractions. However, this added power comes with deep technical challenges.

In this post, we’ll introduce the idea of type-directed macros, show concrete examples with a for-each loop that specializes for different container types, and explore how the Lean theorem prover's elaborators relate to this concept. We’ll also discuss the tricky problem of establishing type contexts during macro expansion and the role of lazy typechecking in making this idea sound.

A Motivating Example: Type-Directed for-each

Let’s start with a simple example: a for-each loop that works over multiple container types like arrays, lists, and sets. In a traditional language, we might write:

for (x in container) {
    print(x)
}

But how this loop works depends on the type of container. Is it an array? A linked list? A set? Under the hood, the loop should expand into different code specialized for each.

In a language with type-directed macros, we could define a macro that inspects the type of container and generates appropriate code:

for (x in container) {
   body
}

If container is an Array<T>, the macro might expand to:

for (let i = 0; i < container.length; i++) {
   let x = container[i];
   body
}

If container is a List<T>, it could expand into:

let current = container;

while (current != null) {
   let x = current.head;
   body current = current.tail;
}

And for a Set<T>:

for (let x of container.iter()) {
   body
}

This kind of specialization is impossible with traditional syntactic macros, because they don’t know the type of container. But with type-directed macros, the macro system can query the typechecker to guide the expansion.

Lean’s Elaborators: A Related Idea

The Lean theorem prover already uses a similar concept called elaborators. In Lean, when you write an expression, it first passes through an elaboration phase, where placeholders (_), overloaded symbols, and implicit arguments are resolved based on type information.

Lean allows users to write custom elaborators, effectively making type-directed macros possible within its logical framework. For example, Lean users can define new syntax that elaborates differently depending on types — much like our for-each example.

However, Lean’s elaborator approach comes with some limitations:

• Global vs. Local Type Context: In Lean, type information flows from the context outward. But when elaborating a complex term, local type information may not be fully known yet. This can make some type-driven macros awkward or fragile.
• Error Handling and Backtracking: Lean’s elaboration system supports backtracking, trying multiple elaboration paths until one typechecks. While powerful, this can make it hard to reason about when and how your elaborator runs.
• Rigid Separation: Elaborators in Lean are deeply tied to its logical kernel and proof assistant infrastructure. General-purpose languages often want more lightweight and modular macro systems.

The Hard Problem: Establishing Type Contexts

The biggest technical challenge with type-directed macros is establishing the type context during macro expansion. Types are normally computed after syntax is fully parsed and expanded. But type-directed macros need types to decide how to expand — creating a chicken-and-egg problem.

For example, consider this hypothetical code:

for (x in myContainer) {
   use(x)
}

To expand this macro:

• The macro system needs to know the type of myContainer.
• But normally, myContainer's type is determined during typechecking, which happens after macro expansion.

This circular dependency is the core difficulty in designing type-directed macros.

The Solution: Lazy Typechecking and Deferral

One practical solution is to allow lazy typechecking for some expressions. Instead of immediately typechecking every subexpression during macro expansion, the system can defer typechecking until enough context is available.

In our for-each case:

• The macro can emit code that refers to myContainer without fully typechecking it yet.
• Later, during typechecking, the system will verify that the expanded code is sound.

This lazy approach enables macros to work with expressions that would otherwise be impossible to handle safely during early expansion. For instance, the macro can generate different code paths for Array<T>, List<T>, and Set<T>, all while deferring the final type resolution until later.

However, this strategy requires careful design to ensure type soundness:

• Deferred expressions must not be executed before they’re typechecked.
• The macro system must track which parts are “pending” and ensure they eventually typecheck in a valid context.

Conclusion: The Future of Macros is Type-Directed

Type-directed macros promise a new level of power and abstraction for programming languages. By leveraging type information during macro expansion, developers can write safer and more flexible code that adapts based on types.

In LSTS we are trying to finish this feature during this month’s sprint. This type-directed approach will replaced the previous pure preprocessor driven macros.