The Essence of Generalized Algebraic Data Types

Explore a comprehensive 18-minute conference talk from POPL 2024 delving into the essence of Generalized Algebraic Data Types (GADTs). Discover how researchers Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, and Lars Birkedal develop an extension of System Fω with recursive types and internalized type equalities, demonstrating direct encodings of GADTs in a minimal lambda-calculus. Learn about the increased expressive power of the calculus through non-macro-expressibility results and its type-soundness proof. Examine two relational models: a unary model showcasing a novel two-stage interpretation technique, and a binary model enabling formal reasoning about data abstraction with GADTs. Access supplementary materials, including reusable artifacts, to deepen your understanding of this advanced topic in functional programming language theory.

[POPL'24] The Essence of Generalized Algebraic Data Types