Tagless-Final Optimizations, Algebraically and Semantically

• Introduction
• Main ideas
• Lecture Materials
• Conclusions
•  
• Sound and Efficient Language-Integrated Query -- Maintaining the ORDER
  A real-life example of the semantic optimizations: transformations and optimizations of language-integrated queries

Introduction

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:

• 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 BY queries.

References

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.

• Multiple interpretations: write once, interpret many times
• Extensibility
• Types
  • typed implementation language
  • typed object language
  • typed optimization rules
  • connections with logic
• Denotations
  • seek meaning
  • algebras
  • evaluation rather than rewriting

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.

• basic_gates.ml [11K]
  Basic gates
• algebra.ml [10K]
  Tagless-final and algebras
• Algebra.hs [9K]
  The Haskell version of algebra.ml, for contrast and to highlight different aspects of tagless-final as algebras
• What is algebra, anyway?
• nand.ml [2K]
  Tagless-final compilation
• 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: earnest normalization-by-evaluation
• 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.

Conclusions

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.