WG211/M24Kovacs

I present a small language implementation which supports the following: dependent types, runtime code generation with cross-stage persistence and full type safety, a builtin monad for effects (mutation, IO). The API of runtime code generation is kept as simple as possible, in order to make it easy to add to existing dependently typed languages, without changing core theories. On the other hand, the runtime semantics is a bit more complicated. During code generation, arbitrarily programs may be evaluated in the presence of free variables. This is called "open evaluation". Fortunately, open evaluation is necessarily already specified for any dependently typed language, since it's used in dependent type checking.