Practical implementation of a dependently typed functional programming language
Practical implementation of a dependently typed functional programming language
复制标题
依赖类型函数式编程语言的实际实现
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Edwin C. Brady
中科院分区：
文献类型：
--
作者：
Edwin C. Brady
类型表示程序的含义，检查类型确保程序具有预期的含义。在依赖类型的编程语言中，类型是基于值的，这使得在其类型中表达程序行为的不变量成为可能。依赖类型允许我们赋予程序更详细的含义，因此对它们的正确性更有信心。本文考虑了使用McBride和McKinna定义的Epigram符号的独立类型编程语言的实际实现。Epigram是一种高级符号，用于独立类型的函数式编程，它阐述了一种基于lujos UTT的核心类型理论，使用Dybjer的归纳族和消除规则来实现模式匹配。这为我们提供了一个丰富的程序推理框架。然而，幼稚的实现引入了一些运行时开销，因为类型系统模糊了类型和值之间的区别；这些开销包括值的重复、冗余信息的存储和明确的证明。任何编程语言的实际实现都应该尽可能高效；在本文中，我们将看到如何克服依赖类型编程的明显效率问题，并且在许多情况下，更丰富的类型信息允许我们应用传统语言中无法直接获得的优化。我介绍了感应族的三种存储优化；强迫，分离和崩溃。我进一步介绍了从核心类型理论到G-machine代码的编译方案，包括用于消除规则的模式匹配编译器和用于高效运行时实现Peano自然数的编译方案。我们还看到了一些低级优化，用于删除恒等函数、未使用的参数和不可能的情况分支。因此，我们看到依赖类型理论是构建可行编程语言的有效基础。
Types express a program's meaning, and checking types ensures that a program has the intended meaning. In a dependently typed programming language types are predicated on values, leading to the possibility of expressing invariants of a program's behaviour in its type. Dependent types allow us to give more detailed meanings to programs, and hence be more confident of their correctness. This thesis considers the practical implementation of a dependently typed programming language, using the Epigram notation defined by McBride and McKinna. Epigram is a high level notation for dependently typed functional programming elaborating to a core type theory based on Lu๙s UTT, using Dybjer's inductive families and elimination rules to implement pattern matching. This gives us a rich framework for reasoning about programs. However, a naive implementation introduces several run-time overheads since the type system blurs the distinction between types and values; these overheads include the duplication of values, and the storage of redundant information and explicit proofs. A practical implementation of any programming language should be as efficient as possible; in this thesis we see how the apparent efficiency problems of dependently typed programming can be overcome and that in many cases the richer type information allows us to apply optimisations which are not directly available in traditional languages. I introduce three storage optimisations on inductive families; forcing, detagging and collapsing. I further introduce a compilation scheme from the core type theory to G-machine code, including a pattern matching compiler for elimination rules and a compilation scheme for efficient run-time implementation of Peano's natural numbers. We also see some low level optimisations for removal of identity functions, unused arguments and impossible case branches. As a result, we see that a dependent type theory is an effective base on which to build a feasible programming language.