The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied. We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages
翻译:无函数化翻译是从程序中消除高阶函数的关键部分,并且它是许多编译器的一部分。然而,依赖类型语言的无函数化还没有被正式研究。我们介绍了第一个针对依赖类型语言进行形式化规定的无函数化翻译,并建立了关键的元理论性质,如:完备性和类型保留性。该翻译适用于依赖类型语言的类型保留编译器。