Implementing domain-specific languages using dependent types and partial evaluation

Edwin Brady

School of Computer Science
University of St Andrews

Thursday, 7 January 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: In this talk, I will describe the efficient implementation of domain-specific languages (DSLs) in Idris, a dependently typed functional programming language. I will show that partial evaluation can be an effective and, unusually, straightforward technique for the efficient implementation of DSLs. We achieve this by exploiting dependent types and by following some simple rules in the definition of the DSL interpreter. I will present experimental evidence that partial evaluation of programs in domain-specific languages yields efficient residual programs whose performance is competitive with their Java and C equivalents and which are also, through the use of dependent types, verifiably resource-safe. Using this technique, it follows that a verifiably correct and resource-safe program can also be an efficient program.

Tarmo Uustalu
Last update 13 January 2010