A classic SSA computation — a counting loop — written in continuation-passing style (CPS).
A switch to direct style that adds higher-order functions and parametric polymorphism.
A demonstration of MimIR's defining trait: types are ordinary values, computed in the same graph as terms — the basis for dependent types.

Under the hood, MimIR is not a list of instructions but a graph. The let bindings in the examples below are pure surface sugar — they only name subexpressions. Inlining them or adding more yields the exact same graph, because in MimIR the graph is the program.

Syntax

Before we dive in, here is just enough Mim syntax to read the examples. Much of it is merely syntactic sugar over that graph: let names a subexpression, where groups binders for readability, and fun / return is sugar for threading an explicit return continuation. lam is a direct-style function that returns a value; con is just sugar for a lam whose return type is ⊥. Equivalently, Cn A is sugar for A → ⊥; this matters in the CPS section below. {} carries implicit arguments, usually types. Tuples are written (a, b, c), and tuple types are written [A, B, C]; more generally [x: A, B x] is a dependent pair type. Arrays are written «i: n; T» or just «n; T» when the element type does not mention the index, while packs are written ‹i: n; v› or ‹n; v› and represent homogeneous tuple terms. So «n; Nat» is the type of length-n arrays of naturals, and ‹n; 0› is the pack of n zeros. Finally, Idx n is the finite type of n indices. So Idx 3 is inhabited by 0₃, 1₃, 2₃. In particular, Idx 2 is just Bool, with 0₂ = ff and 1₂ = tt, so (f, t)#cond simply indexes the two-element tuple (f, t) with the boolean cond.

Plugins

MimIR's built-in language is deliberately tiny: functions, applications, tuples, and the like. Everything domain-specific — arithmetic, comparisons, memory, control-flow helpers, even entire DSLs — lives in plugins. Plugins can sit at any level you like: from low-level bit-fiddling all the way up to full-blown domain-specific operations such as regular expressions. A plugin has two halves that share one name:

a .mim file that declares the plugin's annexes, and
a shared library that registers their runtime behavior: normalizers and plugin-specific compiler phases.

The examples below use the %core plugin throughout, hence the plugin core; at the top of each file.

Annexes

An annex is any entity a plugin exports; you reference it with the %plugin.path syntax, such as %core.wrap.add or %core.select from the %core plugin. Annexes come in two flavors: Axioms and other definitions.

Axioms

These are opaque primitives with no Mim definition. Their meaning comes from the plugin's C++ side (see below), not from any Mim code. %core.wrap.add (machine addition) and %core.pe.is_closed (which checks whether an expression contains no free variables) are treated as axioms.

Axioms get their behavior from normalizers: small C++ functions that live inside the plugin's shared library, each attached to an axiom. Whenever a node is constructed, MimIR fires the matching normalizer eagerly, on the fly — so the simplified node is the only one that ever exists. Constant folding and peephole rewrites such as x + 0 → x are implemented exactly this way: you never build %core.wrap.add (x, 0) and optimize it away later — it collapses to x at construction time.

Other Definitions

These are ordinary Mim values, written as plain Mim. %core.select, for instance, is just

lam %core.select {T: *} (cond, t, f): T = (f, t)#cond;

Being a direct-style function, it carries the default tt filter, which tells MimIR to β-reduce its applications eagerly during graph construction. So a call %core.select (a, b, c) is inlined on the spot, collapsing to the indexed read (c, b)#a — the select itself never appears in the graph.

SSA via CPS

Let's start with a plain counting loop. In C, summing 0 + 1 + … + (n-1) looks like this:

int count(int n) {
    int i = 0, acc = 0;
    while (i < n) {
        acc += i;
        i   += 1;
    }
    return acc;
}

A compiler lowers this into SSA form: basic blocks, φ-functions for the loop-carried i and acc, and explicit branches. In LLVM-style textual IR:

define i32 @count(i32 %n) {
entry:
  br label %loop
loop:                                              ; preds = %entry, %body
  %i    = phi i32 [ 0, %entry ], [ %next, %body ]
  %acc  = phi i32 [ 0, %entry ], [ %sum,  %body ]
  %cond = icmp ult i32 %i, %n
  br i1 %cond, label %body, label %exit
body:
  %next = add i32 %i, 1
  %sum  = add i32 %acc, %i
  br label %loop
exit:
  ret i32 %acc
}

MimIR expresses the same program through the well-established correspondence between SSA form and CPS (see Kelsey'95 and Appel'98): every basic block becomes a continuation (con is a function that never returns). However, in contrast to other CPS representations, functions and other binders in MimIR are scopeless: they are not explicitly nested inside one another. This makes MimIR's take on CPS much more faithful to the original SSA formulation (see Scopeless Binders):

// RUN: %mim -p ll %s
plugin core;
 
fun extern count(n: I32): I32 =
    loop (0I32, 0I32)
    where
        con loop (i acc: I32) =
            let cond = %core.icmp.ul (i, n);
            %core.select (cond, body, exit) ()
            where
                con body() =
                    let next = %core.wrap.add 0 (i, 1I32);
                    let sum  = %core.wrap.add 0 (acc, i);
                    loop (next, sum);
                con exit() = return acc;
            end;
    end;

Correspondence between SSA form and CPS in MimIR:

SSA	MimIR / CPS
basic block	continuation con
φ-function at a block head	continuation parameter (a block argument), e.g. loop (i acc: I32)
φ-argument [ v, pred ]	the value passed at a call site: loop (0I32, 0I32), loop (next, sum)
br label loop (goto)	tail call loop (next, sum)
br i1 cond, body, exit (branch)	%core.select (cond, body, exit) () — pick the target, then apply
ret i32 acc (return)	return acc — call the function's return continuation

The function count itself is written with fun / return: sugar that threads an explicit return continuation through, so it reads like an ordinary function even though it is CPS underneath. As explained in the Plugins section above, the annex %core.select is an ordinary direct-style lambda, so its tt filter makes the branch %core.select (cond, body, exit) collapse to the indexed read (exit, body)#cond during construction — no select node survives. That is what the graph below actually shows.

CPS makes three pieces of SSA folklore explicit:

φ-uses live at the end of a block, not its head.

An SSA φ pretends to read its inputs at the top of its block, but each input is actually produced by a predecessor's terminator — φs "happen on the edge". In CPS the incoming values are simply the arguments passed by the tail call that ends each predecessor — exactly where they are computed.
A whole group of φs at a block head is really a parallel copy.

With block arguments that is plainly one argument tuple per edge, not a pile of pseudo-instructions to sequentialize.
Blocks have honest types.

Cn A is a function from A that never returns and is syntactic sugar for A → ⊥. All basic blocks and even the return point are continuations:
- loop : Cn [I32, I32]
- body, exit : Cn []
- return : Cn I32
In contrast, a traditional basic block carries no type at all.

This is the graph MimIR builds for count:

The MimIR graph of `count` (type edges elided)

Note: Reading the graphs. Each box is a Def — one node of the program graph — labelled with its kind. Boxes drawn with a clipped, diagonal corner are mutable binders (functions and other recursive nodes); plain boxes are immutable, hash-consed expressions. Edges run from a node to its operands.; extern marks count as a root of the program graph. Without it, MimIR's sea-of-nodes cleanup would prune the unused function away.

Scopeless Binders

And here is MimIR's twist. Like traditional basic blocks — which float in the CFG, reached by label rather than by lexical position — every MimIR binder is floating and scopeless. The Mim source nests body and exit inside loop with where, but that nesting exists only in the surface syntax: in the graph there is no containment — body and exit are ordinary nodes the branch indexes into, and loop's back-edge is just an edge from loop to itself. That cycle is well-formed because binders like loop are mutable nodes (drawn with the diagonal corner); everything else stays an acyclic, hash-consed DAG — the sweet spot MimIR hits between a fully mutable and a fully immutable IR.

This is where MimIR diverges from other functional IRs. In a scoped IR a binder lives at a specific point in the nesting, and transformations must keep every variable properly scoped — so the compiler spends real effort moving binders around. MimIR has no scopes: nothing has to move, and there is no lexical scoping to preserve. Two classic chores simply vanish:

β-reduction.

In the following example g does not depend on x. Yet, g is nested inside f. For this reason, a naive β-reduction would superfluously duplicate g as well.
let f x =

let g y = y + 1 in

g (x + 2)

Scoped IRs therefore typically block-float functions independent from the substitution outward before β-reduction to avoid this problem.

MimIR, on the other hand, just β-reduces on the spot. And this is not special to β-reduction: substitution in MimIR is a graph traversal that automatically skips any subgraph not depending on the substituted variables — unrelated binders are left untouched and shared — with no scopes to keep consistent.
Specialization.

In the following example, we want to specialize f for z.
let f x y = x + y in

let g z = (f z 1) + (f z 2)

However, we need to block-sink the specialization fz inside g such that fz's free variable z is now properly scoped:
let g z =

let fz y = z + y in

(fz 1) + (fz 2)

MimIR, on the other hand, does not need block-sinking: a binder simply refers to whatever it refers to, wherever it sits.

And this is not limited to continuations: in MimIR every binder is scopeless — direct-style functions, dependent tuple types, and the rest.

What is more, there is no control-flow graph and no dominator tree. The natural worry is then how do you run any analysis? — SSA leans on dominance for φ-placement, GVN, code motion, etc. MimIR replaces the dominator tree with the nesting tree induced by free variables, and answers liveness/scoping questions by querying a Def's free-variable set directly — computed lazily and memoized. These queries are always correct, even for higher-order code, and the standard SSA optimizations carry over; the construction, its complexity bounds, and its metatheory are spelled out in SSA without Dominance for Higher-Order Programs.

Polymorphic Iteration

CPS is not the only option. MimIR equally supports direct-style functions that simply return a value, and these compose with higher-order functions and polymorphism. The two styles even mix within one curried function: the outer arguments can be direct-style while the final one is a continuation, as in con {T: *} (x: T) = ….

The function iter f (n, x) applies f to x exactly n times. It is polymorphic — the element type T is just another argument, passed implicitly in {} — and recursive. The @(%core.pe.is_closed n) filter is a partial-evaluation directive: whenever n is a constant, MimIR unrolls the recursion away at compile time:

// RUN: %mim %s
plugin core;
plugin refly;
 
lam extern iter {T: *} (f: T → T) (n: Nat, x: T)@(%core.pe.is_closed n): T =
    let cond = %core.ncmp.le (n, 0);
    (%core.select (cond, cons, alt)) () where
        lam cons(): T =
            x;
        lam alt(): T =
            let m = %core.nat.sub (n, 1);
            let y = f x;
            iter @T f (m, y);
    end;
 
lam succ (x: Nat): Nat = %core.nat.add (x, 1);
lam add  (x: Nat) (y: Nat): Nat = iter succ (x, y);
lam mul  (x: Nat) (y: Nat): Nat = iter (add x) (y, 0);
lam pow  (x: Nat) (y: Nat): Nat = iter (mul x) (y, 1);
let _ = %refly.equiv.struc_eq (pow 3 5, 243);

The rest of the file puts iter to work, building a small tower of arithmetic purely by partial application:

succ adds one;
add x y iterates succ — x times, starting from y;
mul x y iterates add x — y times, starting from 0;
pow x y iterates mul x — y times, starting from 1.

Each step hands a partially applied function — add x, mul x — to iter's higher-order parameter f. The final line is a compile-time assertion:

let _ = %refly.equiv.struc_eq (pow 3 5, 243);

Because iter carries the @(%core.pe.is_closed n) partial-evaluation filter — and every function in the tower is direct-style with the default tt filter — MimIR evaluates pow 3 5 completely during graph construction: the whole tower unrolls to the literal 243, and %refly.equiv.struc_eq statically checks it. A mismatch would fail the build.

Now notice what survives. Only iter is extern, hence the sole root. succ, add, mul, pow, and the assertion are all unreachable from the roots, so Cleanup prunes them. The graph MimIR keeps is therefore just iter itself:

The MimIR graph of `iter` — only the `extern` root survives (type edges elided)

The two branches alt and cons are floating functions: MimIR references them as ordinary nodes selected by cond instead of nesting them inside iter, and the recursive call simply points straight back at the iter node. This is MimIR's sea-of-nodes representation in action — the same machinery that expressed the counting loop above, now carrying a higher-order, polymorphic, direct-style function.

You cannot represent this program directly in LLVM or MLIR: iter is polymorphic over T and takes a first-class function as an argument, neither of which those IRs model natively. Getting there requires at least partially lowering the program first — closure conversion for the higher-order arguments, type erasure or monomorphization for the polymorphism, and so on. MimIR represents — and here even partially evaluates — it as written.

Note: Unlike count, iter is a lam in direct style: it returns a T directly instead of threading a return continuation. The same graph substrate represents both styles uniformly.

Types Are Values

So far you have seen higher-order, polymorphic, partially evaluated code in both CPS and direct style. MimIR's defining feature ties all of that together: types live in the same graph as terms, built and normalized by the same machinery. So a type can be computed by an ordinary function, depend on a runtime value, and be partially evaluated — all for free. Watch a type come out of an ordinary function:

// RUN: %mim %s
plugin core;
plugin refly;
 
// `Vec` is an ordinary `lam` — but it returns a *type*: it is a function `Nat → *`.
lam extern Vec (n: Nat): * = «n; Nat»;
 
// `zeros n` builds a length-`n` array of zeros.
// Its return *type* `Vec n` mentions the *value* `n`: a dependent function type.
lam extern zeros (n: Nat): Vec n = ‹n; 0›;
 
// `zeros 3` is partial-evaluated to `‹3; 0›` during graph construction; assert it statically.
let _ = %refly.equiv.struc_eq (zeros 3, ‹3; 0›);

Vec is just a lam — but it returns *, the type of types, so it is a function Nat → *: a type constructor. zeros then has a dependent function type: its return type Vec n mentions the value n of its argument. Nothing special happens to make this work — Vec n is β-reduced to «n; Nat» during construction exactly like %core.select above, even though the result is a type — and %refly.equiv.struc_eq statically checks that zeros 3 evaluates to ‹3; 0›.

The MimIR graph of `Vec` and `zeros` with type edges shown (type edges are dashed)

The same variable node n feeds both the array type «n; Nat» and the array value ‹n; 0› — a type pointing straight at a term. Types are not an earlier, separate phase that has been erased before the IR begins; they are ordinary nodes, hash-consed, normalized, and partially evaluated alongside everything else. This is the foundation the %tensor plugin builds on: array shapes live in the types and are checked — and optimized — by the very same normalization you have already seen.

Table of Contents