SHF: SMALL: A New Semantics for Type-Level Programming in 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.