Generic Programming with Extensible Data Types: Making Ad Hoc Extensible Data Types Less Ad Hoc

Explore a novel approach to generic programming over extensible data types in this 30-minute conference talk from ICFP 2023. Delve into how row types capture the structure of records and variants, expressing record and variant subtyping, record extension, and modular composition of case branches. Learn about extending row typing to capture generic programming over rows themselves, covering patterns such as lifting operations to records and variations from component types, and the duality between case blocks over variants and records of labeled functions. Discover the formalization of this approach in System R𝜔, an extension of F𝜔 with row types, and examine its denotational semantics in Agda. Access the full article and supplementary archive for a deeper understanding of this innovative technique in generic programming.