We’ve been working on a sibling to GHC core with support for linear logic. Our work began with the need to model ownership of physical resources, while also ensuring that the induced calculus has a clean compilation story for good performance. We decided to borrow good ideas in GHC core, our work has been concurrent with and complementary to the recent line of work around join points and sequent calculus, which naturally extend to linear logic

In addition to modeling our problem domain well, linear logic can clarify many ideas ghc already has, but in a uniform way. It provides a natural description of one-shot thunks and internalizes certain fundamental concurrency/parallelism constructs while ensuring resource isolation. We can perhaps provide clearer foundations for how IO and ST style state tokens are reasoned about. Equipping function spaces with explicit unboxed tuples (as telescopes) for both domain and codomain increases the expressivity of core. Finally, as GHC adds more dependently typed features, a sound notion of irrelevance is an important tool for optimization by proof erasure and arises naturally in this work.

We will present the problems which lead to this line of work, our formalization in Agda, possibly a working prototype, and future work.

Work in progress on formalizing this effort can be found at https://github.com/cartazio/system-lf