Weeknotes 2025-W36 › A long-awaited publication: Controlling unfolding in type theory [01GE]

I’m delighted to finally be able to say that my paper Controlling unfolding in type theory with Daniel Gratzer, Carlo Angiuli, Thierry Coquand, and Lars Birkedal is finally accepted with minor revisions to Mathematical Structures in Computer Science. This paper proposes a theoretical and practical foundation for managing the unfolding of complicated definitions in proof assistants—or, shall I say, it proposed the first steps toward such a foundation in 2022 when we submitted it for publication, and we have learned a lot since then.

In the meanwhile, the ideas of the paper have been incorporated into the Agda Proof Assistant by the incomparable Amélia Liao and Jesper Cockx. This has been an extraordinary opportunity for us to learn about the strengths and weaknesses of our idea in practice; although opaque definitions (“controlled unfolding” in the terminology of our paper) seem to be well-liked within the Agda community, there are a number of areas for improvement that we are working on. For example, my student Zhiyi Liu spent a summer internship adapting the framework to allow top-level dependent record types to be “unfolded” into \(\Sigma \)-types to enable a certain level of generic programming for algebraic structures; Zhiyi’s work was in the context of a clean-room prototype, but it could be interesting to implement more seriously.

There are other improvements that I am thinking about with Carlo Angiuli that I can’t talk about just now, but suffice to say that the future of “breakable abstractions” is bright. In my job talk at the Computer Laboratory, I said:

The great semanticist John Reynolds famously wrote in 1983 that “type structure is a syntactic discipline for enforcing levels of abstraction”. If the last twenty years of programming language semantics and verification have taught us anything, it is that we also need a syntactic discipline for breaking abstraction — in other words, a way to glue together programs and verifications that cut across abstraction barriers.

I believe in my statement above even more now than ever.