Staging with Class - A Specification for Typed Template Haskell

This course focuses on teaching multi-stage programming using typed code quotation, specifically addressing the challenges that arise when dealing with type classes in Haskell. The learning outcomes include understanding the interaction between quotation and type classes, resolving this interaction with staged type class constraints, and ensuring type soundness in both source and core programs. Participants will learn about incorporating type classes into multi-stage programs with confidence. The course covers topics such as code generation, well-typedness, well-stagedness, level-indexed constraint resolution, and type-directed elaboration. The teaching method involves presenting recent research work through a formalized source calculus that elaborates into an explicit core calculus. This course is intended for programmers interested in multi-stage programming, code generation, and incorporating type classes into their programs.