The university library will be closed from December 20, 2025 to January 11, 2026. From January 12, 2026, regular opening hours will apply again. Exception: The main medical library and the central library will be open again from January 5, 2026. Further information
  • Generic Programming with Exten...

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

Title:
Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Authors:
Hubers, Alex, Morris, J. Garrett
Publication Year:
2023
Collection:
Computer Science
Subject Terms:
Computer Science - Programming Languages
Document Type:
Report Working Paper
Access URL:
http://arxiv.org/abs/2307.08759
Accession Number:
edsarx.2307.08759
Database:
arXiv

Further information

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.
Comment: To appear at: International Conference on Functional Programming 2023 Corrected citations from previous version