Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang

Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs. We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus that elaborates into an explicit core calculus F. We show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations. Our design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation.

Download / Links
Paper, presented at POPL 2022
Video, presented at POPL 2022

Valid XHTML 1.0! Valid CSS!

Andres Löh, 2022-07-11