Typer: An exocompiler to program with dependent types

在这个项目中，我提出了Typer系统的开发。type是一种实验性编程语言，支持依赖类型和元编程。它基于一个相当标准的核心函数式语言，类似于Agda和Coq，其语法结构受到Lisp语言家族的启发。但与Agda和Coq被设计为证明助手相反，type主要被设计为一种编程语言，其中代码性能的实际问题是一个重要的标准。type的目标与Scheme相似：提供一种小型的核心语言，在其基础上通过元编程提供额外的功能。例如，模块系统和模式匹配是借助\emph{宏}实现的。这种通过库扩展语言的能力是该语言最初的主要目标之一。但是\emph{效率}是一种很大程度上不受这种元编程控制的功能。对于许多程序来说，这是一个问题，在这些程序中，代码最终会对编译器将使用的优化和编译策略做出假设。例如，可能在假设编译器将正确消除尾部递归的情况下编写函数，如果编译器碰巧不使用此优化，则导致不可接受的堆栈消耗，编码器无法告诉编译器他期望什么，编译器也无法指示何时未使用优化。因此，在这个项目中，我建议允许库不仅扩展语言，而且扩展编译器本身。可以说，当前的设计已经使得在库中编写传统上被认为是\emph{编译}的部分内容成为可能。例如，提供模式匹配的宏执行通常称为\emph{模式匹配编译}的操作。但我建议推广这个想法，并尝试将编译器的许多其他部分移到库中，通过实现一个\emph{外编译器}，即一个简化为框架的编译器，专注于提供扩展点，在这些扩展点上，重要的编译决策可以由编译程序本身做出，通常是通过库。

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 fromthe Lisp family of languages. But contrary to Agda and Coq which were designed as proof assistants, Typer is mainly designed as a programminglanguage, 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 betaken by the compiled program itself, typically via libraries.