Tutorial 3

Embedded Domain-specific Language Implementation using Dependent Types

Edwin Brady

Abstract

Domain-specific languages (DSLs) are programming languages designed for solving problems in a particular domain. By providing suitable abstractions, they allow experts to focus on solving high-level problems without being concerned with low-level programming details. Embedded domain-specific languages (EDSLs) are an emerging implementation technique, in which features of a host language, for example parsing or code generation, are exploited by the DSL implementation. In this way, EDSLs can be implemented much more rapidly than their standalone equivalents and can take advantage of compiler optimisations and other implementation effort in the host.

Dependent types allow types to be predicated on values. Using dependent types, a programmer can ascribe a precise type to a program, for example that concatenating lists of length n and m yields a list of length n + m, or that sorting a list of length n yields a list of length n which is a permutation of its input satisfying a given ordering. In this way, types can be viewed as a form of specification, verified by the type checker.

Using a dependently typed language as the host for an EDSL brings additional benefits. Not only can we reuse the host language’s parser and code generator, we can exploit its type system to express properties of the EDSL and guarantee their correctness. In this tutorial I will introduce I DRIS, a dependently typed functional programming language. I will give practical examples of dependently type programs, culminating in the construction of an EDSL for network protocol implementation.

Author biography

Edwin Brady is a SICSA Advanced Research Fellow in Computer Science at the University of St Andrews, where he has worked since receiving his PhD from the University of Durham in 2005. His research interests include functional programming with dependent types, type theory, program generation and programming language design and implementation. His previous work has included compilation and optimisation techniques for dependently typed functional programming languages. This has important applications in the verification of safety-critical systems; he has also been closely involved with the Hume project (http://www.hume-lang.org/), applying dependent type systems to the correct implementation of safety-critical embedded systems with limited memory. He is the main developer of I DRIS (http://www.idris-lang.org/), a functional language with dependent types intended for systems programming, and contributes to the development of Epigram (http://www.e-pig.org/). His recent work has focused on the practical applications of dependently typed programming, using I DRIS to implement domain-specific languages for verified network protocols, data formats, and resource aware systems in general.