Type Safe Reflective Metaprogramming

The template facility of C++, through some serendipity, provides powerful support for metaprogramming and compile-time reflection. However, C++ also has many shortcomings, making C++ template metaprograms inefficient and difficult to maintain. Garcia introduces a calculus for reflective metaprogramming in his thesis that provides all of the power and flexibility of C++ templates and solves many of its problems. However, one of the problems that remains is that the residual program is not type checked until after meta computation is complete. Ideally, one would like the type system of the metaprogram to also guarantee that the residual program will type check, as is the case in MetaML. However, reflective metaprogramming includes computation over types, making the MetaML guarantee difficult to achieve. In this talk we discuss two approaches to dealing with this problem. The first approach catches type errors as early as possible by incrementally type checking code fragments as they are created and spliced together during meta computation. The second and more ambitious approach represents residual programs as generalized algebraic datatypes and relies on the type system of the metaprogramming language to guarantee that residual program is well typed.

Speaker Details

Jeremy Siek is an Assistant Professor at the University of Colorado at Boulder. Jeremy’s areas of research include generic programming, programming language design, type systems, and compiler optimizations for high-level languages. Jeremy received his Ph.D. at Indiana University in 2005 for his thesis “A Language for Generic Programming” which laid the foundation for the constrained templates feature that will appear in the next version of the C++ Standard. Also while at Indiana, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. After leaving Indiana, Jeremy was a post-doc at Rice University with Walid Taha. While at Rice Jeremy worked on the Concoqtion project, melding the MetaOCaml language with the Coq theorem prover and Jeremy developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on a gradually-typed version of Python and on a language for reflective metaprogramming with his graduate students at CU.

Date:
Speakers:
Jeremy Siek
Affiliation:
University of Colorado at Boulder