Metaprogramming via Dependent Types
Published: 2021-08-24
Tags: computics
Abstract
In general, metaprogramming is implemented in a type-unsafe way i.e. it ignores type information in generated code. This is often considered satisfactory since type-checking is still performed at compile-time, so code generation cannot introduce new runtime errors that would be caught at compile-time by type-checking the generated code. However, a type-safe approach offers a much more robust way to provide expressive metaprogramming capabilities in a way that naturally parallels the use of the base language. For example. this approach extends naturally to safe tactics.
Table of Contents
Metaprogramming
Metaprogramming is the design of programs that generate code
meant to be used at the same of a similarly high level of abstraction as
the metaprogram's language. For example, the popular languages Python
and Javascript each provide a built-in function called eval
that takes as input a string and then tries to interpret that
string as a piece of code in the respective language (here, "interpret"
refers to immediately executing the code a high level rather than first
compiling that code to a low-level representation, usually C or
Assembly).
Metaprogramming is the ultimate abstraction tool, since (almost) any pattern of code at all can be generated by a metaprogram of the same or smaller size (asymptotically, at the very least). However, metaprogramming can also yield some severe side-effects.
- Generated code is not directly visible while programming, so there is an additional layer of obfuscation between programming and feedback.
- Metaprograms usually only have limited access to static information,
which inferred by the compiler, about the programs to be generated. On
top of this, metaprograms are not usually checked to make sure they
generate valid programs. Python and Javascript's
evalfunction know that their argument is a string and nothing more!