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
Dependent Types
Metaprogramming via Dependent Types
Signature

§ 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 eval function know that their argument is a string and nothing more!

§ Dependent Types

§ Metaprogramming via Dependent Types

§ Signature

The following code block is the Ed25519 signature of this post's markdown content encoded in base 64, using my secret key and public key.

d90d62e596befa74a594f3cd8cf5f64d3052ec6d6d262c1c518bd9897454ffedfc5dca3261aa9160cb66b25b46e81eb57afe6b5a91bacb19d2d2b5a25c810d0f

See Signature for more information.