The Essence of Generalized Algebraic Data Types
summary
Presents a minimal core calculus—System Fω+μ with internalized type equalities and injective constant constructors—that directly encodes GADTs, proves injectivity strictly increases expressiveness (a non‑macro‑expressibility result), and gives syntactic progress/preservation. Builds a syntactic/semantic story: a normalization-based syntactic model plus two-stage unary then binary relational models that surprisingly validate injectivity and support representation‑independence proofs. All results are mechanized and artifacts are available; the models work where naive set interpretations fail.
AI-written summary · about
chapters (7)
- 0:00GADTs introduction
- 1:48Calculus for GADTs
- 6:27Encoding GADTs
- 7:33Semantic modeling challenges
- 9:18Two-stage semantic model
- 13:13Contributions and future work
- 15:26Q&A
related talks
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
12mA Unified View of Modalities in Type Systems
19mInterpreting OCaml GADTs into Coq
14mType-Sensitive Algebraic Macros
22mA Calculus of Inductive Linear Constructions
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
24mA Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F...