Conference proceeding
Abstracting Extensible Data Types: Or, Rows by Any Other Name
Proceedings of ACM on programming languages, Vol.3(POPL), pp.1-28
01/02/2019
DOI: 10.1145/3290325
Abstract
We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic λ-calculus.
Details
- Title: Subtitle
- Abstracting Extensible Data Types: Or, Rows by Any Other Name
- Creators
- J. Garrett Morris - University of KansasJames Mckinna - University of Edinburgh
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of ACM on programming languages, Vol.3(POPL), pp.1-28
- DOI
- 10.1145/3290325
- ISSN
- 2475-1421
- eISSN
- 2475-1421
- Grant note
- DOI: 10.13039/100000181, name: AFOSR, award: FA8655-13-1-3006
- Language
- English
- Date published
- 01/02/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259405102771
Metrics
23 Record Views