Staging with Class - A Specification for Typed Template Haskell

Explore multi-stage programming and typed code quotation in Haskell through this conference talk from YOW! 2022. Delve into the challenges of integrating type classes with quotation in Haskell and discover a proposed solution: staged type class constraints. Learn about the formalization of this approach in a source calculus that elaborates into an explicit core calculus. Examine type soundness in both calculi and understand how well-typed, well-staged source programs are guaranteed to elaborate into well-typed, well-staged core programs. Investigate beta and eta rules for code quotations and gain insights into incorporating type classes into multi-stage programs confidently. While focused on Haskell, explore how this foundation can be applied to other languages supporting both overloading and quotation. Follow the presentation's progression from introductory concepts to advanced topics, including level-indexed constraint resolution, evaluation of staged programs, and type-directed elaboration.

Intro
Quotations and splices
Multi-stage programming: example
Code generation
Multi-stage programming and type classes
Multi-stage programming: well-typedness
Well-stagedness: the level of an expression
Well-stagedness: the level restriction
Is the problem with qpower well-stageness?
Well-staged type classes
Key idea: staged type class constraints
Level-indexed constraint resolution
How to evaluate staged programs?
Level-indexed Evaluation
Key idea: splice environments
Type-directed elaboration
Integration into GHC