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
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
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:
- implement a simple but realistic and usable DSL of logical circuits
(hardware description language)
- write many interesting transformations, such as constant
propagation, conversion to normal forms, and simplification --
in small and easily composable steps.
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
- 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.
- Let's start with the refrain, to be heard
throughout the course.
- Multiple interpretations:
write once, interpret many times
- typed implementation language
- typed object language
- typed optimization rules
- connections with logic
- seek meaning
- evaluation rather than rewriting
- 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
- basic_gates.ml [11K]
- algebra.ml [10K]
Tagless-final and algebras
- What is algebra, anyway?
- nand.ml [2K]
- bneg_adhoc.ml [4K]
Pushing the negation down, in an ad hoc way
- bconst_prop.ml [5K]
Boolean constant propagation, in a systematic way. The question of correctness
- cnf.ml [7K]
Conversion to the conjunctive normal form in one easy step:
- circuit.ml [13K]
From gates to circuits; circuit optimizations
We also introduce record types (to describe ports: collection of
labeled wires), in a semi-static--typing sort of way. We explain
the spectrum of static--dynamic typing, and point out that
in a code-generation setting, dynamic typing on an
earlier stage amounts to a static typing of the later stage.
- Tagless-final optimizations are possible. They are modular,
composable, and type-preserving. This course has emphasized two
- 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;