Staging with Class: A Specification for Typed Template Haskell

Ningning Xie; Matthew T Pickering; Andres Loh; Nicolas Wu; Jeremy Yallop; Meng Wang

doi:10.1145/3498723

Staging with Class: A Specification for Typed Template Haskell

Ningning Xie, Matthew T Pickering, Andres Loh, Nicolas Wu, Jeremy Yallop, Meng Wang

Department of Computer Science

Research output: Contribution to journal › Article (Academic Journal) › peer-review

6 Citations (Scopus)

59 Downloads (Pure)

Abstract

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.

Original language	English
Article number	61
Number of pages	30
Journal	Proceedings of the ACM on Programming Languages
Volume	6
Issue number	POPL
DOIs	https://doi.org/10.1145/3498723
Publication status	Published - 12 Jan 2022

Bibliographical note

Funding Information:
We thank Dimitrios Vytiniotis, and the anonymous reviewers for their insightful comments. The work is partly supported by EPSRC Grant SCOPE: Scoped Contextual Programming with Effects (EP/S028129/1) and Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1).

Publisher Copyright:
© 2022 Owner/Author.

Research Groups and Themes

Programming Languages

Keywords

Staging
Type Classes
Typed Template Haskell

Access to Document

10.1145/3498723

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery at 10.1145/3498723. Please refer to any applicable terms of use of the publisher.
Final published version, 404 KBLicence: CC BY

Handle.net

Persistent link

Embargoed Document

Full-text PDF (accepted author manuscript)
Accepted author manuscript, 988 KB
Request copy

8030 EPSRC EP/T008911/1 EXHIBIT : Expressive High-Level Languages for Bidirectional Transformations
Wang, M. (Principal Investigator)
1/07/20 → 30/06/23
Project: Research

Cite this

@article{452179a7887e4ddda4460c8a526799ab,

title = "Staging with Class: A Specification for Typed Template Haskell",

abstract = "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.",

keywords = "Staging, Type Classes, Typed Template Haskell",

author = "Ningning Xie and Pickering, {Matthew T} and Andres Loh and Nicolas Wu and Jeremy Yallop and Meng Wang",

note = "Funding Information: We thank Dimitrios Vytiniotis, and the anonymous reviewers for their insightful comments. The work is partly supported by EPSRC Grant SCOPE: Scoped Contextual Programming with Effects (EP/S028129/1) and Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1). Publisher Copyright: {\textcopyright} 2022 Owner/Author.",

year = "2022",

month = jan,

day = "12",

doi = "10.1145/3498723",

language = "English",

volume = "6",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - Staging with Class

T2 - A Specification for Typed Template Haskell

AU - Xie, Ningning

AU - Pickering, Matthew T

AU - Loh, Andres

AU - Wu, Nicolas

AU - Yallop, Jeremy

AU - Wang, Meng

N1 - Funding Information: We thank Dimitrios Vytiniotis, and the anonymous reviewers for their insightful comments. The work is partly supported by EPSRC Grant SCOPE: Scoped Contextual Programming with Effects (EP/S028129/1) and Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1). Publisher Copyright: © 2022 Owner/Author.

PY - 2022/1/12

Y1 - 2022/1/12

N2 - 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.

AB - 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.

KW - Staging

KW - Type Classes

KW - Typed Template Haskell

U2 - 10.1145/3498723

DO - 10.1145/3498723

M3 - Article (Academic Journal)

SN - 2475-1421

VL - 6

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 61

ER -

Staging with Class: A Specification for Typed Template Haskell

Abstract

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Embargoed Document

Fingerprint

Projects

8030 EPSRC EP/T008911/1 EXHIBIT : Expressive High-Level Languages for Bidirectional Transformations

Cite this