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

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

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.