SHF: SMALL: A New Semantics for Type-Level Programming in Haskell

SHF：SMALL：Haskell 中类型级编程的新语义

• 批准号: 2345580
• 负责人: John Garrett Morris
• 金额: $ 59.93万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-07-01 至 2027-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2345580&HistoricalAwards=false
• 关键词: SHF; SMALL; New; Semantics; Type

The project sits at the intersection of two important goals in practical and correct software development. The first is precisely and formally capturing the requirements of programs and program components: one does not want a program to rely on comparing functions for equality or adding arbitrary integers to pointers. The second is modular and extensible program construction: program components must be developed independently and changes internal to one component should not cause cascading changes to other components. This project's novelties are: a new foundation for extensible descriptions of program properties and invariants, subsuming multiple competing and complementary features used in current languages; its implementation; and its metatheory. The project's impacts are: regularizing and extending features for specifying program properties in existing languages; simplifying their implementation; and making these features practical for adoption in other languages.The primary focus of this project is the programming language Haskell. Haskell has an advanced type system with several features for modular and extensible specification of program properties, most prominently type classes and type families. These features have evolved mostly independently, with different approaches to their specification and implementation. The result, for both programmers and implementers, is a constellation of features with frequently surprising interactions and limitations. This project develops a new core language for Haskell, with a single feature that captures both type classes and type families. It will simplify Haskell implementations and make the existing features of Haskell more regular and more expressive. It will enable new features of Haskell, closing the gaps between type families and type classes. And, it will make it easier for other languages to adopt features from Haskell, by giving them a simpler underlying semantics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

该项目位于实用和正确的软件开发中的两个重要目标的交集。 第一个是精确和正式捕获程序和程序组件的要求：一个人不希望程序依靠比较功能以平等或将任意整数添加到指针中。 第二个是模块化和可扩展的程序构建：必须独立开发程序组件，并且内部组件内部的变化不应导致其他组件的级联变化。 该项目的新颖性是：针对程序属性和不变式的可扩展描述的新基础，涵盖了当前语言中使用的多个竞争和互补功能；其实施；和它的元害。 该项目的影响是：以现有语言指定程序属性的正规化和扩展功能；简化其实施；并使这些功能以其他语言采用。该项目的主要重点是编程语言Haskell。 Haskell具有一个高级类型系统，具有多个功能，用于对程序属性的模块化和可扩展规范，最突出的类型类和类型的家庭。 这些功能主要是独立发展的，采用了不同的规范和实施方法。 对于程序员和实施者而言，结果是具有经常令人惊讶的交互和局限性的功能。 该项目为Haskell开发了一种新的核心语言，其单个功能可以捕获类型类和类型的家庭。 它将简化Haskell的实现，并使Haskell的现有功能更加规律，更具表现力。 它将启用Haskell的新功能，缩小类型家庭和类型类之间的差距。 而且，这将使其他语言更容易通过给予简单的基础语义来采用Haskell的功能。该奖项反映了NSF的法定任务，并且使用基金会的知识分子优点和更广泛的影响评估标准，认为值得通过评估值得支持。