Repository logo
 

Staging with class: A specification for typed template Haskell

Published version
Peer-reviewed

Type

Article

Change log

Authors

Xie, N 
Pickering, M 
Löh, A 
Wu, N 
Yallop, J 

Abstract

jats:pMulti-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:italicF</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:pOur 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>

Description

Keywords

Staging, Type Classes, Typed Template Haskell

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

Journal ISSN

2475-1421
2475-1421

Volume Title

6

Publisher

Association for Computing Machinery (ACM)