一句话：提出 staged type class constraints，形式化为源演算 λ⇒ 与核心演算 F，证明类型健全性，解决代码引用与类型类的不健全交互。
多阶段编程常借助带类型安全的代码引用（typed quotation）来编写优化代码生成器，但在 Haskell 中代码引用与类型类（type class）交互不健全，导致分阶段程序难以正确编写。本文研究这一不健全性，并提出 staged type class constraints 作为解决方案，将其形式化为源演算 λ⇒，并精化到显式核心演算 F。作者证明了两个演算的类型健全性，即类型良好且分阶段良好的源程序总能精化为类型良好且分阶段良好的核心程序，同时给出了代码引用的 beta 与 eta 规则。该设计以 Haskell 为动机，但也可作为支持重载与引用的其他语言的基础。
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.
@article{paperbot1547,
title = {Staging with class: a specification for typed template Haskell},
author = {Ningning Xie and Matthew Pickering and Andres Löh and Nicolas Wu and Jeremy Yallop and Meng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498723}
}