Journal article
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Proceedings of ACM on programming languages, Vol.7(ICFP), pp.356-384
08/31/2023
DOI: 10.1145/3607843
Appears in UI Libraries Support Open Access
Abstract
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.
Details
- Title: Subtitle
- Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
- Creators
- Alex Hubers - University of IowaJ. Garrett Morris - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Proceedings of ACM on programming languages, Vol.7(ICFP), pp.356-384
- DOI
- 10.1145/3607843
- ISSN
- 2475-1421
- eISSN
- 2475-1421
- Publisher
- Association for Computing Machinery (ACM)
- Grant note
- name: NSF, award: CCF-2044815
- Language
- English
- Date published
- 08/31/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984464481402771
Metrics
15 Record Views