Typer: An exocompiler to program with dependent types

Typer：用于使用依赖类型进行编程的外编译器

• 批准号: RGPIN-2018-06225
• 负责人: Monnier, Stefan
• 金额: $ 1.68万
• 依托单位: Université de Montréal
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679455
• 关键词: Typer; exocompiler; program; 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.**

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