A Specification for Typed Template Haskell
Matthew Pickering, Andres L\"oh, Nicolas Wu
TL;DR
This paper introduces a formal core semantics for Typed Template Haskell, enabling predictable multi-stage programming with polymorphism and qualified types, bridging source language and core calculus.
Contribution
It provides the first formal semantics for Typed Template Haskell, integrating multi-stage programming with polymorphism and qualified types.
Findings
Formal semantics relating source and core languages
Supports multi-stage programming with polymorphism
Enhances predictability of code generation
Abstract
Multi-stage programming is a proven technique that provides predictable performance characteristics by controlling code generation. We propose a core semantics for Typed Template Haskell, an extension of Haskell that supports multi staged programming that interacts well with polymorphism and qualified types. Our semantics relates a declarative source language with qualified types to a core language based on the the polymorphic lambda calculus augmented with multi-stage constructs.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Parallel Computing and Optimization Techniques