Typer: An exocompiler to program with dependent types

点击翻译按钮获取中文摘要

In this project, I propose the development of the Typer system. Typer is an experimental programming language with support for dependent types and metaprogramming. It is based on a fairly standard core functional language similar to that of Agda and Coq, with a syntactic structure inspired from***the Lisp family of languages. But contrary to Agda and Coq which were designed as proof assistants, Typer is mainly designed as a programming***language, where practical issues of performance of the code is an important criterion.******Typer has similar goals to Scheme: provide a small core language on top of which additional functionality is provided via metaprogramming. For example, the module system and the pattern-matching are implemented with the help of \emph{macros}. This ability to extend the language via libraries was one of the main original goals of the language.******But \emph{efficiency} is a kind of functionality that's largely out of the control of this kind of metaprogramming. This is a problem for many programs where the code ends up making assumptions about the kind of optimization and compilation strategies the compiler will use. For example, a function might be written under the assumption that the compiler will properly eliminate tail recursion, resulting in unacceptable stack consumption if the compiler happens not to use this optimization, with no way for the coder to tell the compiler what he expects, nor for the compiler to indicate when the optimization was not used.******So in this project, I propose to allow libraries to extend not just the language but the compiler itself. Arguably the current design already makes it possible to write parts of what is traditionally considered \emph{compilation} in libraries. For example the macro that provides pattern matching performs what is usually called \emph{pattern match compilation}. But I propose to generalize this idea and try and move many other parts of the compiler to libraries, by implementing an***\emph{exocompiler}, i.e.~a compiler reduced to a skeleton that focuses on providing extension points where the important compilation decisions can be***taken by the compiled program itself, typically via libraries.**