Staging with class: A specification for typed template Haskell
View / Open Files
Authors
Xie, N
Pickering, M
Löh, A
Wu, N
Yallop, J
Wang, M
Publication Date
2022Journal Title
Proceedings of the ACM on Programming Languages
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Volume
6
Issue
POPL
Pages
1-30
Type
Article
This Version
VoR
Metadata
Show full item recordCitation
Xie, N., Pickering, M., Löh, A., Wu, N., Yallop, J., & Wang, M. (2022). Staging with class: A specification for typed template Haskell. Proceedings of the ACM on Programming Languages, 6 (POPL), 1-30. https://doi.org/10.1145/3498723
Abstract
<jats:p>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.</jats:p>
<jats:p>
We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus λ
<jats:sup>⇒</jats:sup>
that elaborates into an explicit core calculus
<jats:italic>F</jats:italic>
. 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.
</jats:p>
<jats:p>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.</jats:p>
Identifiers
External DOI: https://doi.org/10.1145/3498723
This record's URL: https://www.repository.cam.ac.uk/handle/1810/333404
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk