一句话：提出两级类型论，将依赖类型编译期语言与无闭包一阶对象语言结合，保证抽象不产生运行时闭包。
函数式编程中的 monadic bind 等高阶抽象常依赖通用编译器优化来消除运行时闭包，但 GHC 等无法提供强保证，用户只能通过内联指令和选项间接控制代码生成。本文提出一种两阶段语言：对象语言是简单类型一阶语言，可无运行时闭包地编译；编译期语言是依赖类型论；两者整合为两级类型论。作者展示两个应用：用 staging 开发 monad 与 monad transformer，复用 Haskell 生态中的大部分定义并消除抽象开销；用依赖类型给出 pull-based stream fusion，其中 concatMap 可保证融合。工作提供 Agda 实现及带类型 Template Haskell 实现。
Many abstraction tools in functional programming rely heavily on general-purpose compiler optimization to achieve adequate performance. For example, monadic binding is a higher-order function which yields runtime closures in the absence of sufficient compile-time inlining and beta-reductions, thereby significantly degrading performance. In current systems such as the Glasgow Haskell Compiler, there is no strong guarantee that general-purpose optimization can eliminate abstraction overheads, and users only have indirect and fragile control over code generation through inlining directives and compiler options. We propose a two-stage language to simultaneously get strong guarantees about code generation and strong abstraction features. The object language is a simply-typed first-order language which can be compiled without runtime closures. The compile-time language is a dependent type theory. The two are integrated in a two-level type theory. We demonstrate two applications of the system. First, we develop monads and monad transformers. Here, abstraction overheads are eliminated by staging and we can reuse almost all definitions from the existing Haskell ecosystem. Second, we develop pull-based stream fusion. Here we make essential use of dependent types to give a concise definition of a concatMap operation with guaranteed fusion. We provide an Agda implementation and a typed Template Haskell implementation of these developments.