Second International Summer School on Metaprogramming
From the tagless-final cookbook: simple hardware description language and optimization-by-evaluation
Oleg Kiselyov (Tohoku University, Japan)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 optimization rules 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.
Using a familiar example and the OCaml language, the tutorial will explain the general framework of embedding and optimizing DSLs.
Meta-F*: efficient meta-programming of the F* compiler at every stage
Jonathan Protzenko (Microsoft Research)F* is an ML-inspired, dependently-typed programming language equipped with an effect system and a weakest precondition calculus. F* traditionally supports program verification through the use of an SMT solver. Recently, we extended F* into Meta-F*, which gives the programmer powerful and fine-grained control over the F* compiler via a principled discipline of meta-programs. Meta-programs can extend the compiler for new language features, proof automation, and meta-generation of stateful programs.
In this series of lectures, I will present F* itself, followed by the design and implementation of Meta-F*. I will show how meta-programs leverage all the features of the F* type system and are written in a dedicated effect that captures the interaction with the compiler. I will illustrate the features of Meta-F* with examples taken from Project Everest, a large-scale verification effort that uses F* at its core, and relies heavily on the features of Meta-F*.
Building Languages with Racket
Matthew Flatt (University of Utah)Racket is an extensible programming language that allows programmers to define syntactic forms, create embedded domain-specific languages (DSLs), and construct entirely new programming languages. We'll provide a refresher on Lisp-style extensibility, cover Scheme-style pattern-matching and procedural macros, and delve into Racket-specific topics like redefining implicit macros, the syntax-parse library, and macros that cooperate through compile-time information.
Exploring Universes
Conor McBride (University of Strathclyde)Dependent type theory allows us to compute types and programs from data. A universe is a collection of types given as the image of a function, often for a perfectly ordinary datatype. In these lectures, I'll construct some universes which expose particular structure. In particular, I'll focus on the structure which makes some data types syntaxes. By capturing the notion of syntax, we take a step towards uniformity in the presentation of semantics.
Programming with nominal techniques
Jamie Gabbay (University of Strathclyde)Nominal techniques are an approach to names and binding with applications to datatypes of abstract syntax with binding, but also non-syntactic structures such as orbit-finite sets (nominal automata), modal logics, name-carrying function-spaces, and more. We can trace this broad applicability to the mathematical foundations on which nominal techniques are based: namely, sets with atoms.
This raises an interesting question: how can we implement the power of nominal techniques inside an existing programming language? After all, that programming language was probably designed using a model based on ordinary sets, without atoms (... or was it?).
It's worth noting that we don't need the full power of sets with atoms: we just need to encode enough behaviour to do interesting and useful examples, preferably in a transparent and portable manner that allows the user to appeal to a "nominal" user model, but embedded in the framework of some specific implementation.
Trying to identify a useful subset of atoms-like behaviour, and match it up to the constructs available in a given language (exceptions? references?) is a subtle design issue. The applications of a solution are clear -- bringing nominal techniques to the programmers' workbench -- but I also believe that solutions in this design space may provide a new way of understanding the motivating mathematics.
I will sketch two attempts at modelling nominal techniques in an existing programming language, motivate the design space, and then leave it as an exercise to the audience to complete and/or correct, embellish, or supercede my designs in a language of their choice, the results to be collated and made available on GitHub and potentially made into an academic publication.
Steps towards structured multi-stage programming
Jeremy Yallop (University of Cambridge)Multi-stage programming (writing programs that generate programs) is a useful tool for eliminating the overhead introduced by abstraction. Unfortunately, a naive approach to staging typically produces disappointing results, such as generated programs that are large and inefficient.
I'll sketch some recent techniques and constructs that offer a more sophisticated approach to multi-stage programming, incorporating algebraic simplifications and supporting flexible generation of recursive programs.