Understanding the interaction between elaboration and quotation

  • Matthew T Pickering

Student thesis: Doctoral ThesisDoctor of Philosophy (PhD)


Multi-stage programming languages have long promised programmers the means to program libraries with specific performance guarantees. Despite this, the adoption into mainstream high-level languages such as Haskell, Scala and OCaml has been very slow. In particular, our focus, Typed Template Haskell has been implemented for a number of years but the ecosystem has failed to adopt the multi-stage ideas. The situation hasn’t been helped by a number of soundness and expressivity issues with the current implementation.

In this thesis we tackle the problem of soundly combining multi-stage features with other features as commonly found in modern programming languages. The main contribution is the design and implementation of a language which combines multiple stages with implicit arguments and an elaboration phase. The goal is to provide a firmer foundation for future implementations and to enable library writers to use multi-stage features with confidence in conjunction with the rest of the Haskell language.
Date of Award23 Mar 2021
Original languageEnglish
Awarding Institution
  • The University of Bristol
SupervisorSteven Ramsay (Supervisor)

Cite this