This SkillsCast is currently only available to registered attendees of YOW! Lambda Jam 2022
It will be freely available to all Skills Matter members once the YOW! Lambda Jam 2022 early-access window expires on August 17, 2022.
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. In this talk, I will present my recent work which studies this unsound interaction and proposes a resolution, staged type class constraints, which is formalized in a source calculus that elaborates into an explicit core calculus. I will 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. The 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.