dc.contributor.author | Morris, J. Garrett | |
dc.contributor.author | McKinna, James | |
dc.date.accessioned | 2018-12-14T18:25:27Z | |
dc.date.available | 2018-12-14T18:25:27Z | |
dc.date.issued | 2019 | |
dc.identifier.citation | J. Garrett Morris and James McKinna. 2019. Abstracting Extensible Data Types: Or, Rows by Any Other Name.
Proc. ACM Program. Lang. 3, POPL, Article 12 (January 2019), 28 pages. https://doi.org/10.1145/3290325 | en_US |
dc.identifier.uri | http://hdl.handle.net/1808/27514 | |
dc.description.abstract | | en_US |
dc.description.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. | |
dc.publisher | Association for Computing Machinery | en_US |
dc.rights | This work is licensed under a Creative Commons Attribution 4.0 International License. © 2019 Copyright held by the owner/author(s). | en_US |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en_US |
dc.subject | Extensible data types | en_US |
dc.subject | Row types | en_US |
dc.subject | Row polymorphism | en_US |
dc.subject | Qualified types | en_US |
dc.title | Abstracting Extensible Data Types: Or, Rows by Any Other Name | en_US |
dc.type | Article | en_US |
kusw.kuauthor | Morris, J. Garrett | |
kusw.kudepartment | Electrical Engineering and Computer Science | en_US |
dc.identifier.doi | 10.1145/3290325 | en_US |
kusw.oaversion | Scholarly/refereed, author accepted manuscript | en_US |
kusw.oapolicy | This item meets KU Open Access policy criteria. | en_US |
dc.rights.accessrights | openAccess | en_US |