Syntax Micros🔗

An implementation of micros on top of macros.

Macros syntax? into syntax?, both representing arbitrary source terms. Roughly, their type is Source -> Source. They are very flexible and can be useful for language extenisble and shallow-embedding DSL implementation. Unfortunately, as their output is arbitrary source terms (possibly including more macro definitions), it is difficult to stop macro expansion, for example because you want to stop at a fixed intermediate representation (IR).

Micros instead expand to a well-defined IR (Krishnamurthi 2001), not necessarily represented as syntax objects. That is, micros have type Source -> IR. Micro expansion is easy to stop, and simplifies writing arbitrary processing over the IR outside of the macro expander.

This library implements micros as a pattern over macros. Micro languages can be embedded in Racket by first elaborating from syntax to an IR, then preprocessing, then continuing elaboration into Racket. This is similar to syntax-spec-v3 (Ballantyne et al. 2024); however, syntax-spec-v3 provides a fixed core language definition, represented as syntax objects. Micros provide an extensible core language definition, whose representation is arbitrary and generated by the micro definition. (syntax-spec-v3 provides lot of other features as well, such as macros scoped to a particular DSLs.)

1 Tutorial: STLC🔗

Using micros, we can easily implement hybrid embedding of DSLs into Racket. Compared to pure macro embeddings, this allows us to use traditional AST representation instead of syntax objects, and use traditional traversal techniques, instead of relying on the macro expander.

In this tutorial we’ll implement an embedding of the simply-typed lambda calculus. Our micros expand to a struct representation, giving us a traditional efficient AST representation. We can then easily implement the traditional bidirectional typechecker, followed by a compilation back into Racket as syntax objects. This approach requires fewer new abstractions compared to the macro embedding approach of turnstile  (Chang et al. 2017), although with less extensibility, although some extensibility could be achieved using define-generics to implement the type checker.

We’ll start by defining two micro languages: one for terms, and one for types. Conceptually, we need one micro language for each non-terminal. Each micro define an extensible parser or elaborator from the source language into the core IR.

The types are simple, so we can use define-simple-micro, which generates the micro and its struct representation. We’ll define two types: natural numbers and functions.

Next we can start defining terms. We’ll embed Racket naturals using a define-embedding-micro, and define functions and applications.

Now that the entire language is defined, we can implement a standard bi-directional type checker by matching against the entire syntax tree. We could have also decided to implement the type checker using define-generics, so the type checker itself is extensible. We define two functions: type-check and type-synth.

We could continue this exercise, wrapping the result into a hash-lang. See examples/stlc-hashlang.rkt in the repository for an extended example.

2 Reference🔗

These functions will raise an error until micros are defined for name-id.

For convenience, a struct definition may be attached and will be defined in the scope of the micro definition, as it may be common to use structs to represent IR terms. If specified, struct-spec should be syntax that can be passed to struct, starting with the option super-id. The struct will also be named kw-id, which will be defined at phase 1.

Expands stx fully to some micro language. The returns syntax object is arbitrary, but has the micro IR attached using syntax/mule. binds should specify any free identifiers in scope, and what to expand them into. Their expansion should be a IR in the same micro language.

Bibliography🔗