Thu 20 Jan 2022 15:05 - 15:30 at Salon III - Metaprogramming Chair(s): Stephanie Weirich

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.

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template HaskellInPerson
POPL
Ningning Xie University of Toronto, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
DOI Media Attached
15:30
25m
Research paper
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
DOI Media Attached
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
DOI Media Attached