Tagless-Final Optimizations, Algebraically and Semantically

The course ``From the Tagless-Final Cookbook: Embedding and Optimizing (Hardware) Domain-Specific Languages in the Tagless-Final Style'' has been presented at the Second International Summer School on Metaprogramming <https://www.cl.cam.ac.uk/events/metaprog/2019/> at Schloss-Dagstuhl, Germany, August 11-16, 2019.

This page collects the course materials, in the form of the extensively commented OCaml code.



The ``tagless-final'' style is a general method of embedding (often typed) domain-specific languages (DSL) in a typed functional language such as Haskell, OCaml, Scala and Coq. Once written, a DSL expression may be interpreted many times. Evaluator, compiler, partial evaluator, pretty-printer are all interpreters. At any time one may add more interpreters, and even more expression forms to the DSL while re-using the previous interpreters as they were. Only well-typed DSL terms are representable. Therefore, the type checker of the host language checks -- and even infers for us -- DSL types.

It was recently discovered how to transform, simplify, and generally, optimize DSLs embedded in this style. The optimizations are reusable, modular, composable, and type- and scope-preserving by construction.

In this incarnation of the course we expound the denotational/algebraic perspective on DSL optimization, using as the running example a simple hardware description DSL.

By the end of the tutorial, the participants will:


The presented framework has been used for real-life projects, such as the compositional and extensive language-integrated query. It is the first such system able to optimize ORDER BY queries.

Modular, composable, typed optimizations in the tagless-final style
The earlier course (CUFP 2015, Metaprogramming Summer School 2016) on tagless-final optimizations
The present course is a variant, but not the repetition. Although the same DSL of combinational circuits is used, it is now developed at a faster pace and to a larger extent. Mainly, the present course expounds a semantic rather than syntactic approach, focusing on denotations rather than on term rewriting.


Main ideas

Let's start with the refrain, to be heard throughout the course.


Lecture Materials

The tagless-final style has been successfully used in Haskell, OCaml, Scala and even to some extent in Rust and Java. The tutorial thus should be applicable across the modern (functional) programming languages. For the actual presentation one programming language had to be chosen, which happens to be OCaml. Only passing familiarity with OCaml will be assumed from the audience. The tutorial will introduce all necessary language features, with comments how they may be realized in other languages.

The tutorial is meant to be interactive: interacting with the audience and with the OCaml interpreter, working through problems with active audience participation. The following is the complete OCaml source code that was presented and interacted with during the lectures. It has been amended to reflect questions and comments of the participants. The code is extensively commented: the comments are the lecture notes. No libraries or packages beyond the standard library are needed to run the code: the most basic OCaml installation should suffice.



Tagless-final optimizations are possible. They are modular, composable, and type-preserving. This course has emphasized two perspectives:
Algebraic perspective
What are the operations? Write them down. Has some subset of them already been considered and implemented? Is the DSL or the optimization at hand an extension of an already solved problem?
Denotational perspective
What do we eventually want? Imagine it! Define it! And then think how to compute it.

The tutorial has numerous quizzes: search for ``QUIZ'' in the source code files. Other good exercises are: selective inlining (combine only those circuits when doing so will not lead to duplication); writing the optimizations of the sort AND x x -> x; earnest Boolean simplification; converting to DNF; handling sharing.