Partial Evaluation in Dependently Typed Languages

依赖类型语言中的部分求值

• 批准号: 2589772
• 金额: --
• 依托单位: University of St Andrews
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2589772
• 关键词: Partial; Evaluation; Dependently; Typed; Languages

This project aims to explore the optimisation of dependently typed programming languages using partial evaluation. In addition to answering open researchquestions, the project will provide a concrete implementation of a partial evaluator for the Idris2 compiler. The project furthers the research already undertaken by Brady[4], aiming to make dependently typed languages practical forwriting everyday programs through the careful application of program optimisations.Partial evaluation (PE) is an optimisation technique which evaluates portionsof the program at compile time to produce a more efficient executable[7]. It is apowerful generalisation of constant folding, which allows programmers to writeidiomatic definitions without loss of performance. Many modern programminglanguages implement PE, with some inferring the areas of program to evaluate,and with others taking explicit guidance from the programmers (for example,C++11's constexpr keyword). The main drawback to partial evaluation is thatit can be very expensive for large programs, significantly increasing compilationtimes.

该项目旨在探索使用部分求值的依赖类型编程语言的优化。除了回答开放的研究问题外，该项目还将为Idris2编译器提供部分评估器的具体实现。该项目进一步推进了Brady b[4]已经开展的研究，旨在通过仔细应用程序优化，使独立类型语言在编写日常程序时变得实用。部分求值（PE）是一种优化技术，它在编译时对程序的部分求值，以产生更有效的可执行程序。它是常量折叠的强大泛化，它允许程序员在不损失性能的情况下编写习惯定义。许多现代编程语言都实现了PE，其中一些语言推断出要评估的程序领域，而另一些语言则从程序员那里得到明确的指导（例如，c++ 11的constexpr关键字）。部分求值的主要缺点是，对于大型程序来说，它可能非常昂贵，显著地增加了编译时间。