• View
• Edit
• History
• Print

DependentTypesForDSLs

Dependent Types for DSLs

by Edwin Brady

(an invited talk at the DSL4EE workshop, 2011)

Abstract

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.

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 a language 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.

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 talk I will introduce Idris, a dependently typed functional programming language, and show, interactively and by example, how it can be used to implement domain specific languages for modelling resource usage.