RUI:Initial Algebra Packages for GADTs: Principled Tools for Structured Programming

0700341 Patricia JohannRutgersU用于GADT的初始代数包：结构化编程的原则性工具通用代数数据类型(GADT)处于函数式编程的前沿，并日益广泛使用。然而，GADT的基础还没有得到很好的理解。这项研究的目的是证明GADT支持与其他高级数据类型相同的初始代数语义，并使用这种语义来派生表达和原则性工具的集合-称为初始代数包-用于理解GADT结构、构造操纵这些结构的程序、推理这些程序的性质以及自动改进以模块构造的此类程序的性能。该研究采用三部分方法来获得GADT的初始代数语义和程序包。首先，为每个GADT导出一个等价的嵌套类型；其次，导出这些嵌套类型的初始代数语义和包。最后，使用嵌套类型的初始代数语义和包来推导其对应的GADT的初始代数语义和包。通过为GADT提供推理、编程和优化工具，这项研究有可能为程序员提供比目前可用的更广泛的有效处理数据的选择，从而通过使程序能够更好地构造和操作数据来改进编程。

0700341Patricia JohannRutgers U Initial Algebra Packages for GADTs: Principled Tools for Structured ProgrammingGeneralized algebraic data types (GADTs) are at the cutting edge of functional programming, and become more widely used every day. Nevertheless, the foundations of GADTs are not well understood. This research aims to show that GADTs support the same kind of initial algebra semantics as other advanced data types, and to use this semantics to derive collections of expressive and principled tools --- called initial algebra packages --- for understanding GADT structures, structuring programs which manipulate those structures, reasoning about properties of those programs, and automatically improving the performance of modularly constructed such programs. The research employs a three-part approach to deriving initial algebra semantics and packages for GADTs. First, an equivalent nested type is derived for each GADT.Secondly, initial algebra semantics and packages for these nested types are derived. Finally, the initial algebra semantics and packages for the nested types are used to derive initial algebra semantics and packages for their corresponding GADTs. By providing reasoning, programming, and optimization tools for GADTs, this research has the potential to offer programmers a wider range of options for effectively handling data than is currently available, and thus to improve programming by enabling programs to better structure and manipulate data.