Mazeppa

Supercompilation [^turchin-concept] is a program transformation technique that symbolically evaluates a given program, with run-time values as unknowns. In doing so, it discovers execution patterns of the original program and synthesizes them into standalone functions; the result of supercompilation is a more efficient residual program. In terms of transformational power, supercompilation subsumes both deforestation [^deforestation] and partial evaluation [^partial-evaluation], and even exhibits certain capabilities of theorem proving.

Mazeppa is a modern supercompiler intended to be a compilation target for call-by-value functional languages. Having prior supercompilers diligently compared and revised, Mazeppa

Provides the full set of primitive data types for efficient computation.
Supports manual control of function unfolding.
Is fully transparent in terms of what decisions it takes during transformation.
Is designed with efficiency in mind from the very beginning.

Installation

First, install the OCaml system on your machine:

$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup

Then clone the repository and install Mazeppa:

$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh

Type mazeppa --help to confirm the installation.

<details> <summary>Building with Flambda</summary>

Flambda is a powerful program inliner and specializer for OCaml. If you build Mazeppa with an Flambda-enabled OCaml compiler, you may see much better performance. To set it up:

$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)

(You may use a different version instead of 5.2.0 if you wish.)

To check if Flambda was successfully enabled, run:

$ ocamlopt -config | grep flambda

</details>

Hacking

You can play with Mazeppa without actually installing it. Having OCaml installed and the repository cloned (as above), run the following command from the root directory:

$ ./scripts/play.sh

(Graphviz is required: sudo apt install graphviz.)

This will launch Mazeppa with --inspect on playground/main.mz and visualize the process graph in target/graph.svg. The latter can be viewed in VS Code by the Svg Preview extension.

./scripts/play.sh will automatically recompile the sources in OCaml, if anything is changed.

Supercompilation by example

The best way to understand how supercompilation works is by example. Consider the following function that takes a list and computes a sum of its squared elements:

[examples/sum-squares/main.mz]

main(xs) := sum(mapSq(xs));

sum(xs) := match xs {
    Nil() -> 0i32,
    Cons(x, xs) -> +(x, sum(xs))
};

mapSq(xs) := match xs {
    Nil() -> Nil(),
    Cons(x, xs) -> Cons(*(x, x), mapSq(xs))
};

This program is written in the idiomatic, listful functional style. Every function does only one thing, and does it well. However, there is a serious problem here: mapSq essentially constructs a list that will be immediately deconstructed by sum, meaning that we 1) we need to allocate extra memory for the intermediate list, and 2) we need two passes of computation instead of one. The solution to this problem is called deforestation [^deforestation], which is a special case of supercompilation.

Let us see what Mazeppa does with this program:

$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect

The --inspect flag tells Mazeppa to give a detailed report on the transformation process. The sum-squares/target/ directory will contain the following files:

target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json

graph.dot contains the complete process graph for our program. You can obtain a picture of the graph by running dot -Tsvg target/graph.dot > target/graph.svg.
nodes.json contains the contents of all nodes in the graph. Without this file, you would not be able to understand much from the graph alone.
program.json contains the initial program in Mazeppa IR: our supercompiler works with this particular representation instead of the original program.
output.mz contains the final residual program.

output.mz will contain the following code:

[examples/sum-squares/target/output.mz]

main(xs) := f0(xs);

f0(x0) := match x0 {
    Cons(x1, x2) -> +(*(x1, x1), f0(x2)),
    Nil() -> 0i32
};

The supercompiler has successfully merged sum and mapSq into a single function, f0! Unlike the original program, f0 works in a single pass, without having to allocate any extra memory.

How did the supercompiler got to this point? Let us see the generated process graph:

For reference, nodes.json contains the following data in JSON:

[
  [ "n0", "main(xs)" ],
  [ "n1", "sum(mapSq(xs))" ],
  [ "n2", "sum(.g1(xs))" ],
  [ "n3", "xs" ],
  [ "n4", "sum(Cons(*(.v0, .v0), mapSq(.v1)))" ],
  [ "n5", ".g0(Cons(*(.v0, .v0), mapSq(.v1)))" ],
  [ "n6", "+(*(.v0, .v0), sum(mapSq(.v1)))" ],
  [ "n7", "+(*(.v0, .v0), sum(.g1(.v1)))" ],
  [ "n8", "*(.v0, .v0)" ],
  [ "n9", ".v0" ],
  [ "n10", ".v0" ],
  [ "n11", "sum(.g1(.v1))" ],
  [ "n12", ".v1" ],
  [ "n13", "+(.v3, .v4)" ],
  [ "n14", ".v3" ],
  [ "n15", ".v4" ],
  [ "n16", "sum(Nil())" ],
  [ "n17", ".g0(Nil())" ],
  [ "n18", "0i32" ]
]

(We will not need to inspect program.json for this tiny example, but feel free to look at it: it is not too complicated.)

The supercompiler starts with node n0 containing main(xs). After two steps of function unfolding, we reach node n2 containing sum(.g1(xs)), where .g1 is the IR function that corresponds to our mapSq. At this point, we have no other choice than to analyze the call .g1(xs) by conjecturing what values xs might take at run-time. Since our mapSq only accepts the constructors Nil and Cons, it is sufficient to consider the cases xs=Cons(.v0, .v1) and xs=Nil() only.

Node n4 is what happens after we substitute Cons(.v0, .v1) for xs, where .v0 and .v1 are fresh variables. After three more function unfoldings, we arrive at n7. This is the first time we have to split the call +(*(.v0, .v0), sum(.g1(.v1))) into .v3=*(.v0, .v0) (n8) and .v4=sum(.g1(.v1)) (n11) and proceed supercompiling +(.v3, .v4) (n13); the reason for doing so is that a previous node (n2) is structurally embedded in n7, so supercompilation might otherwise continue forever. Now, what happens with sum(.g1(.v1)) (n11)? We have seen it earlier! Recall that n2 contains sum(.g1(xs)), which is just a renaming of sum(.g1(.v1)); so we decide to fold n11 into n2, because it makes no sense to supercompile the same thing twice. The other branches of n7, namely n13 and n8, are decomposed, meaning that we simply proceed transforming their arguments.

As for the other branch of n2, sum(Nil()) (n16), it is enough to merely unfold this call to 0i32 (n18).

After the process graph is completed, residualization converts it to a final program. During this stage, dynamic execution patterns become functions -- node n2 now becomes the function f0, inasmuch as some other node (n11) points to it. In any residual program, there will be exactly as many functions as there are nodes with incoming dashed lines, plus main.

In summary, supercompilation consists of 1) unfolding function definitions, 2) analyzing calls that pattern-match an unknown variable, 3) breaking down computation into smaller parts, 4) folding repeated computations, and 5) decomposing calls that cannot be unfolded, such as +(.v3, .v4) (n13) in our example. The whole supercompilation process is guaranteed to terminate, because when some computation is becoming dangerously bigger and bigger, we break it down into subproblems and solve them in isolation.

There are a plenty of other interesting examples of deforestation in the examples/ folder, including tree-like data structures. In fact, we have reimplemented all samples from the previous work on higher-order call-by-value supercompilation by Peter A. Jonsson and Johan Nordlander [^CbV-supercomp] [^CbV-supercomp-next]; in all cases, Mazeppa has performed similarly or better.

Specializing the power function

Now consider another example, this time involving partial evaluation:

[examples/power-sq/main.mz]

main(a) := powerSq(a, 7u8);

powerSq(a, x) := match =(x, 0u8) {
    T() -> 1i32,
    F() -> match =(%(x, 2u8), 0u8) {
        T() -> square(powerSq(a, /(x, 2u8))),
        F() -> *(a, powerSq(a, -(x, 1u8)))
    }
};

square(a) := *(a, a);

powerSq implements the famous exponentiation-by-squaring algorithm. The original program is inefficient: it recursively examines the x parameter of powerSq, although it is perfectly known at compile-time. Running Mazeppa on main(a) will yield the following residual program:

[examples/power-sq/target/output.mz]

main(a) := *(a, let x0 := *(a, *(a, a)); *(x0, x0));

The whole powerSq function has been eliminated, thus achieving the effect of partial evaluation. (If we consider powerSq to be an interpreter for a program x and input data a, then it is the first Futamura projection: specializing an interpreter to obtain an efficient target program.) Also, notice how the supercompiler has managed to share the argument *(a, *(a, a)) twice, so that it is not recomputed each time anew. The residual program indeed reflects exponentiation by squaring.

Synthesizing the KMP algorithm

Let us go beyond deforestation and partial evaluation. Consider a function matches(p, s) of two strings, which returns T() if s contains p and F() otherwise. The naive implementation in Mazeppa would be the following, where p is specialized to "aab":

[examples/kmp-test/main.mz]

main(s) := matches(Cons('a', Cons('a', Cons('b', Nil()))), s);

matches(p, s) := go(p, s, p, s);

go(pp, ss, op, os) := match pp {
    Nil() -> T(),
    Cons(p, pp) -> goFirst(p, pp, ss, op, os)
};

goFirst(p, pp, ss, op, os) := match ss {
    Nil() -> F(),
    Cons(s, ss) -> match =(p, s) {
        T() -> go(pp, ss, op, os),
        F() -> failover(op, os)
    }
};

failover(op, os) := match os {
    Nil() -> F(),
    Cons(_s, ss) -> matches(op, ss)
};

(Here we represent strings as lists of characters for simplicity, but do not worry, Mazeppa provides built-in strings as well.)

The algorithm is correct but inefficient. Consider what happens when "aa" is successfully matched, but 'b' is not. The algorithm will start matching "aab" once again from the second character of s, although it can already be said that the second character of s is 'a'. The deterministic finite automaton built by the Knuth-Morris-Pratt algorithm (KMP) [^kmp] is an alternative way to solve this problem.

By running Mazeppa on the above sample, we can obtain an efficient string matching algorithm for p="aab" that reflects KMP in action:

[examples/kmp-test/target/output.mz]

main(s) := f0(s);

f0(x0) := match x0 {
    Cons(x1, x2) -> match =(97u8, x1) {
        F() -> f1(x2),
        T() -> f2(x2)
    },
    Nil() -> F()
};

f1(x0) := f0(x0);

f2(x0) := match x0 {
    Cons(x1, x2) -> match =(97u8, x1) {
        F() -> f1(x2),
        T() -> f4(x2)
    },
    Nil() -> F()
};

f3(x0) := f2(x0);

f4(x0) := match x0 {
    Cons(x1, x2) -> match =(98u8, x1) {
        F() -> match =(97u8, x1) {
            F() -> f1(x2),
            T() -> f4(x2)
        },
        T() -> T()
    },
    Nil() -> F()
};

The naive algorithm that we wrote has been automatically transformed into a well-known efficient version! While the naive algorithm has complexity O(|p| * |s|), the specialized one is O(|s|).

Synthesizing KMP is a standard example that showcases the power of supercompilation with respect to other techniques (e.g., see [^perfect-process-tree] and [^positive-supercomp]). Obtaining KMP by partial evaluation is not possible without changing the original definition of matches [^partial-evaluation-matches-1] [^partial-evaluation-matches-2].

Metasystem transition

Valentin Turchin, the inventor of supercompilation, describes the concept of metasystem transition in the following way [^turchin-mst-scp] [^turchin-transformation] [^turchin-dialogue]:

Consider a system S of any kind. Suppose that there is a way to make some number of copies from it, possibly with variations. Suppose that these systems are united into a new system S' which has the systems of the S type as its subsystems, and includes also an additional mechanism which controls the behavior and production of the S-subsystems. Then we call S' a metasystem with respect to S, and the creation of S' a metasystem transition. As a result of consecutive metasystem transitions a multilevel structure of control arises, which allows complicated forms of behavior.

Thus, supercompilation can be readily seen as a metasystem transition: there is an object program in Mazeppa, and there is the Mazeppa supercompiler which controls and supervises execution of the object program. However, we can go further and perform any number of metasystem transitions within the realm of the object program itself, as the next example demonstrates.

We will be using the code from examples/lambda-calculus/. Below is a standard