ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Wed 6 Sep 2023 15:00 - 15:30 at A - Grand Ballroom 2 - Types Chair(s): Alan Jeffrey

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.

Wed 6 Sep

Displayed time zone: Pacific Time (US & Canada) change

15:00 - 16:00
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
ICFP Papers and Events
Alex Hubers University of Iowa, J. Garrett Morris University of Iowa
DOI Pre-print
Typing Records, Maps, and Structs
ICFP Papers and Events
Giuseppe Castagna CNRS; Université Paris Cité