 |
MimIR
MimIR is my Intermediate Representation
|
|
MimIR
MimIR is my Intermediate Representation
|
MimIR is a pure, graph-based, higher-order intermediate representation rooted in the Calculus of Constructions. MimIR provides:
MimIR is well suited for DSL compilers, tensor compilers, automatic differentiation, regex engines, and other systems that need high-performance code from high-level abstractions.
MimIR brings two worlds together: typed functional IRs supply the abstractions β polymorphism, dependent types β while sea-of-nodes graphs supply the performance. It has both at once, by extending sea-of-nodes to the Calculus of Constructions. And it pays off in practice: the regex plugin is the fastest engine in our evaluation (see the POPL'25 paper).
The following function sq squares x β for any type T, as long as T comes packaged with its own multiplication. Then, f instantiates sq for Nat:
That first argument (T: *, mul: [T, T] β T) is a dependent pair β an existential bundling a type together with an operation on it. In MimIR, types are ordinary first-class values: T and mul are just arguments, so polymorphism, type operators, and dependent types all fall out of the same mechanism.
And under the hood, MimIR is not a list of instructions but a graph β and that graph is the program. The graph is also complete: it holds everything needed to make sense of the program, with no auxiliary side structure. Contrast a traditional instruction list, which is meaningless on its own and only becomes intelligible once you pair it with a separately maintained control-flow graph.
Watch what happens to sq. When f applies sq (Nat, core.nat.mul), that application is Ξ²-reduced on the fly, during graph construction β not in any later pass. This is permitted because sq carries the default tt filter that every direct-style function gets, which greenlights inlining. What remains is the bare x * x, with no trace of sq or the existential abstraction. The original sq lambda is now simply unreachable from the world's roots (sq is not extern), so traversing the graph never reaches it; a Cleanup phase later drops it for good:
For the full picture, with more examples and the graphs MimIR builds for them, read the Tour of MimIR. With MimIR's Python bindings, you can write full-blown DSL compilers embedded in Python; see the embedded Python DSL for a complete end-to-end example. Or, naturally, you can continue exploring the rest of the documentation.
| Feature | LLVM | MLIR | MimIR |
|---|---|---|---|
| Higher-order functions | β | β οΈ (regions only) | β (first-class functions) |
| Type operators | β | β | β |
| Parametric polymorphism | β | β | β |
| Higher-kinded polymorphism | β | β | β |
| Dependent types | β | β | β |
| Semantic extensibility | β | π§ (dialect-specific C++ semantics) | β (typed axioms) |
| Program representation | CFG + instruction lists | CFG / regions + instruction lists | Arbitrary expressions (direct style + CPS) |
| Structural foundation | CFG + dominance | CFG / regions + dominance | Free variables + nesting |
| DSL embedding / semantics retention | β¬οΈ Low | β‘οΈ Medium (dialects, lowering) | β¬οΈ High (CC, partial evaluation, typed axioms, normalizers, lowering) |
See the full build options in the Contributing & Debugging guide. New here? Start with the Tour of MimIR.
Declare new types, operations, and normalizers in a single .mim file. For example, the demo plugin declares one axiom and wires it to a C++ normalizer:
The matching shared library implements normalize_const and any lowering or phases; C++ does the heavy lifting of optimization, lowering, and code generation.
Explore the Plugin Registry to discover and share community-developed plugins.
MimIR uses a sea-of-nodes-style program graph and extends it to the Calculus of Constructions with higher-order functions, polymorphism, and dependent types. MimIR hits the sweet spot between a fully mutable IR, which is easy to construct, and a fully immutable IR:
Non-binder expressions are immutable:
Hash-consing, normalization, type checking, and partial evaluation happen automatically during graph construction.
Binders are mutable where needed:
They support variables and recursion by βtying the knotβ through in-place mutation.
Terms and types share one graph:
Terms, types, and type-level computations all live in the same program graph as ordinary expressions.
Forget CFG dominance. MimIR uses free-variable nesting:
Free-variable queries βjust workβ:
This is always correct. MimIR maintains free-variable information lazily, locally, and transparently: results are computed on demand, memoized, and invalidated only where needed. For realistic programs a query costs O(n log n) in the size of the subgraph, and O(1) once memoized (see the PLDI'26 paper).
MimIR is a recursive acronym for MimIR is my Intermediate Representation.
In Norse mythology, MΓmir was a being of immense wisdom. After being beheaded in the ΓsirβVanir War, Odin preserved his head, which continued to speak secret knowledge and offer counsel.
Today, you have MΓmir's head at your fingertips.
Throughout the codebase, we consistently use mim / MIM for namespaces, macros, CMake variables, and related identifiers.
Acknowledgments: We gratefully acknowledge Alex Wendland and the other maintainers of the former MimIR GitHub organization for kindly making the organization name available for this project. The previous organization has been renamed to mimir-depricated.
Ready to build the next generation of DSL compilers?
β Star MimIR on GitHub, join Discord, and let's make high-performance DSLs easy.
MimIR is licensed under the MIT License.
1.16.1 
