---
pubDate: 2021-08-24
title: Metaprogramming via Dependent Types
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: true
---

## 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.

1. Generated code is not directly visible while programming, so there is an
   additional layer of obfuscation between programming and feedback.
2. 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!
3.

## Dependent Types

## Metaprogramming via Dependent Types