MimIR

[TOC]

MimIR is a pure, graph-based, higher-order intermediate representation rooted in the Calculus of Constructions. MimIR provides:

• Higher-order functions, parametric polymorphism, and dependent types out of the box
• Extensible plugins for domain-specific axioms, types, normalizers, and code generation
• SSA without dominance: a scopeless IR for higher-order programs based on free-variable nesting
• A sea-of-nodes style IR with on-the-fly normalization, type checking, and partial evaluation

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](@ref regex) plugin is the fastest engine in our evaluation (see the POPL'25 paper).

✨ A Taste of Mim

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:

\include "sq.mim"

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](@ref mim::Lam::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](@ref mim::World::roots) (sq is not extern), so traversing the graph never reaches it; a [Cleanup](@ref mim::Cleanup) phase later drops it for good:

@image html sq.svg "The MimIR graph of f — the abstraction has evaporated (type edges elided)"

For the full picture, with more examples and the graphs MimIR builds for them, read the [Tour of MimIR](@ref mimir). With MimIR's Python bindings, you can write full-blown DSL compilers embedded in Python; see the [embedded Python DSL](@ref python) for a complete end-to-end example.

💡 Why MimIR?

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)

@note The table compares native IR-level support and representation, not what can be emulated via custom IR extensions, closure conversion, lowering, or external analyses.

🚀 Quick Start

git clone --recursive git@github.com:mimir/mimir.git
cd mimir
cmake -S . -B build -DBUILD_TESTING=ON -DMIM_BUILD_EXAMPLES=ON
cmake --build build -j$(nproc)

📦 Install (Optional)

cmake -S . -B build -DBUILD_TESTING=ON -DMIM_BUILD_EXAMPLES=ON -DCMAKE_INSTALL_PREFIX=/my/local/install/prefix
cmake --build build -j$(nproc) --target install

See the full [build options](@ref building) in the [Contributing & Debugging](@ref coding) guide. New here? Start with the [Tour of MimIR](@ref mimir).

🔥 Key Innovations

🧩 Plugins

Declare new types, operations, and normalizers in a single .mim file. For example, the [demo](@ref demo) plugin declares one axiom and wires it to a C++ normalizer:

/// the 42 constant, folded by the `normalize_const` C++ normalizer
axm %demo.const_idx: [n: Nat] → Idx n, normalize_const;

The matching shared library implements normalize_const and any lowering or [phases](@ref phases); C++ does the heavy lifting of optimization, lowering, and code generation.

Explore the Plugin Registry to discover and share community-developed plugins.

🌊 Sea of Nodes

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](@ref mut) 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.

🪾 SSA without Dominance

Forget CFG dominance. MimIR uses free-variable nesting:

• Free variables replace dominance; the nesting tree replaces the dominator tree

• Free-variable queries “just work”:

  if (expr->free_vars().contains(x))           // x free in expr
  if (expr->free_vars().has_intersection(xyz)) // x, y, or z free in expr

  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).

• Data dependencies remain precise, even for higher-order code

• Loop peeling and unrolling reduce to simple β-reduction

• Mutual recursion and higher-order functions are handled naturally

🐉 Naming: MimIR vs. Mim

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.

• MimIR refers to the graph-based intermediate representation and its C++ API.
• Mim is a lightweight textual representation of MimIR. It is not a full-featured programming language, but provides enough syntactic sugar to concisely express polymorphic and dependent types (including type-level dependencies introduced by many type variables). Mim is mainly intended for defining plugin interfaces and writing small test cases.

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.

💬 Community

• 💬 Discord → Join the chat
• 📚 Documentation → https://mimir.github.io
• 💻 Examples → examples/ and lit/

Ready to build the next generation of DSL compilers?

⭐ Star MimIR on GitHub, join Discord, and let's make high-performance DSLs easy.

⚖️ License

MimIR is licensed under the MIT License.

📖 Publications

• SSA without Dominance for Higher-Order Programs
  Roland Leißa, Johannes Griebler
  
  
  

• MimIrADe: Automatic Differentiation in MimIR
  Marcel Ullrich, Sebastian Hack, Roland Leißa
  
  
  

• MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
  Roland Leißa, Marcel Ullrich, Joachim Meyer, Sebastian Hack