Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc

Alex Hubers; J. Garrett Morris

doi:10.48550/arxiv.2307.08759

Back

Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc

Preprint

Open access

Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc

Alex Hubers and J. Garrett Morris

ArXiv.org

07/17/2023

DOI: 10.48550/arxiv.2307.08759

Files and links (1)

url

https://doi.org/10.48550/arxiv.2307.08759View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. 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{\omega}, an extension of F{\omega} with row types, and give a denotational semantics for (stratified) R{\omega} in Agda.

Computer Science - Programming Languages

Details

Title: Subtitle: Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Creators: Alex Hubers
J. Garrett Morris
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2307.08759
ISSN: 2331-8422
Language: English
Date posted: 07/17/2023
Academic Unit: Computer Science
Record Identifier: 9984445524002771

Metrics

12 Record Views