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.

0700341 Patricia Johannrutgers U初始代数软件包：用于结构化编程的代数数据类型（GADTS）的原始工具处于功能编程的尖端，并且每天都在更广泛地使用。 然而，GADT的基础尚不清楚。这项研究旨在表明，GADTS支持与其他高级数据类型相同类型的初始代数语义，并使用此语义来得出表达性和原则性工具的收集 - 称为初始代数包装 - 理解GADT结构，构造这些结构，这些结构，这些结构，这些结构，对这些程序进行操作，并自动改善这些程序，并自动构建了这些程序，并进行了自动构建的表演。该研究采用三部分的方法来推导GADT的初始代数语义和包装。首先，为每个GADT得出了等效的嵌套类型。第二，这些嵌套类型的初始代数语义和软件包。最后，使用嵌套类型的初始代数语义和包装来推导其相应GADT的初始代数语义和软件包。通过为GADT提供推理，编程和优化工具，这项研究有可能为程序员提供比目前可用的更广泛的选项，以便有效地处理数据，从而通过促进程序来更好地结构和操纵数据来改善编程。