Modern software engineering relies on large ecosystems of independent software components and libraries. This poses two challenges for the design of programming languages and language tooling, both of which are addressed by this project. First, languages must support developing independent components, including identifying and abstracting reusable components from existing applications. Second, languages must provide expressive specification mechanisms to ensure that components are used correctly and that components do not have unintended interactions. The project's novelties are new programming language features for modular specification and implementation of program data and behavior, at all level of the software stack from user-facing applications to operating system components and hardware support. The project's impacts are improvements in both software reliability and programmer productivity, as the project enables language tooling to automatically help programmers identify and correctly use software components and libraries.
The project has two primary themes. The first is modularity and reuse in high-level functional programs. The project develops extensible types for data and computational effects, supporting high-level abstractions including overloading, generic programming, and extensible effect handlers. The second is modularity and reuse in low-level and systems programs. The project develops extensible bit-level specifications of data structures and their layout, targeting applications including operating system kernels and hardware interfaces. Each of these themes will only have impact if the resulting language features have comparable performance with existing approaches. The project uses linear typing and compile-type specialization to offset runtime costs traditionally associated with generic and extensible programming techniques.
J. Garrett Morris, principal investigator
Alex Hubers, graduate research assistant
Apoorv Ingle, graduate research assistant
▷ ▽ Wenhao Tang, Daniel Hillerström, Sam Lindley, J. Garrett Morris, "Soundly Handling Linearity". POPL '24.
We propose a novel approach to soundly combining linear types with multi-shot effect handlers. Linear type systems statically ensure that resources such as file handles and communication channels are used exactly once. Effect handlers provide a rich modular programming abstraction for implementing features ranging from exceptions to concurrency to backtracking. Whereas conventional linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded (e.g. for exceptions) or invoked more than once (e.g. for backtracking). This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control-flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs.
We formalise the notion of control-flow linearity in a System F-style core calculus Feff∘ equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that Feff∘ preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control-flow linearity can be made practical, we adapt Links based on the design of Feff∘, in doing so fixing a long-standing soundness bug.
Finally, to better expose the potential of control-flow linearity, we define an ML-style core calculus Qeff∘, based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control-flow linearity. Both linearity and effects are captured by qualified types. Qeff∘ overcomes a number of practical limitations of Feff∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.
This paper is open access in the ACM DL.
▷ ▽ Alex Hubers and J. Garrett Morris, "Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc". ICFP '23.
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System R𝜔, an extension of F𝜔 with row types, and give a denotational semantics for (stratified) R𝜔 in Agda.
This paper is open access in the ACM DL.
▷ ▽ Alex Hubers and J. Garrett Morris, Rω formalization as of ICFP'23.
Our artifact is an Agda library. The development consists principally of the following components:
A snapshot of this development is available on GitHub