๐พ Archived View for dcreager.net โบ papers โบ Hubers2023.gmi captured on 2023-07-22 at 16:24:39. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
Alex Hubers and J. Garrett Morris. 2023. Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc. Proc. ACM Program. Lang. 7, ICFP, Article 201 (August 2023), 29 pages.
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System R๐, an extension of F๐ with row types, and give a denotational semantics for (stratified) R๐ in Agda.