Intensional Analysis of Typed Template Haskell Quotations
summary
A system desugars Typed Template Haskell quotations into a well-typed PHOAS AST so quoted expressions become inspectable and transformable rather than opaque, implemented as a GHC extension prototype. It exposes variables, lambdas and patterns for optimizers, serialization and EDSL backends, but requires adds external-variable parameter E to handle open terms, uses generics for constructors, must record binder types for safe decoding, and needs nontrivial type‑checker changes; a minimal proof‑of‑concept exists.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:36Limitations of opaque quotations
- 3:42Goals for transparent representations
- 6:59Parametric higher-order abstract syntax with PHZ
- 8:43Identity interpretation
- 10:52Open terms in quotations
- 13:41Constructors and pattern matching
- 15:25Preserving type info
- 16:46Type checker challenges
- 17:47Future work
- 18:36Comparison with Core
- 20:02Implementation status
- 21:46Q&A
related talks
25mStaging with Class: A Specification for Typed Template Haskell
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
42mFunctional interpreters and you
19mIll-Typed Programs Don't Evaluate
15mLogic Programming with Extensible Types (Lightning talk)
25mMonadic typed tactic programming by reflection
59mExpression Templates: Past, Present, Future
20mGenerating Well-Typed Terms that are not "Useless"