2023/07/17 by Alex Hubers, Hubers, Alex, J. Garrett Morris +1 · 1 citation
Computer Science · Decision Sciences · #Advanced Database Systems and Queries #FOS: Computer and information sciences #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL) #Scientific Computing and Data Management
paper · pdf · doi:10.48550/arxiv.2307.08759
openalex publication_date 2023/07/17 · openalex created_date 2023/07/20 · openalex updated_date 2026/07/28
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.