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

该项目位于实际和正确的软件开发的两个重要目标的交叉点。第一个是准确而正式地捕获程序和程序组件的需求：人们不希望程序依赖于比较函数是否相等或将任意整数添加到指针。第二是模块化和可扩展的程序构建：程序组件必须独立开发，一个组件内部的更改不应导致对其他组件的级联更改。这个项目的创新之处在于：为程序属性和不变量的可扩展描述提供了一个新的基础，包含了当前语言中使用的多个相互竞争和互补的功能；它的实现；以及它的元理论。该项目的影响是：规范和扩展用现有语言指定程序属性的功能；简化其实现；使这些功能适用于其他语言。该项目的主要重点是编程语言Haskell。Haskell有一个高级类型系统，具有几个用于程序属性的模块化和可扩展规范的功能，最突出的是类型类和类型族。这些功能基本上是独立发展的，它们的规范和实现方法各不相同。对于程序员和实现者来说，结果是一系列具有经常令人惊讶的交互和限制的功能。该项目为Haskell开发了一种新的核心语言，具有同时捕获类型类和类型族的单一功能。它将简化Haskell的实现，并使Haskell的现有功能更规范、更具表现力。它将启用Haskell的新功能，缩小类型族和类型类之间的差距。而且，通过给予其他语言更简单的底层语义，它将使其他语言更容易采用Haskell的功能。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.