abstract

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: we do 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 impementation; 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.

personnel

J. Garrett Morris, principal investigator

Andrew Marmaduke, postdoctoral researcher

Apoorv Ingle, graduate research assistant

artifacts

Apoorv Ingle and Andrew Marmaduke. System FD formalization in Lean4.

This is a mechanized development of the metatheory of System FD in the Lean4 interactive theorem prover. The development includes:

• The metatheory of System FD itself, including type soundness;
• Translations from a Haskell-like surface language to System FD.

The development is open source, on GitHub