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

RUI：GADT 的初始代数包：结构化编程的原则工具

• 批准号: 0700341
• 负责人: Patricia Johann
• 金额: $ 13.8万
• 依托单位: Rutgers University New Brunswick
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-08-01 至 2009-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0700341&HistoricalAwards=false
• 关键词: RUI; Initial; Algebra; Packages; GADTs

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.

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