Show simple item record

dc.contributor.authorMorris, J. Garrett
dc.contributor.authorMcKinna, James
dc.date.accessioned2018-12-14T18:25:27Z
dc.date.available2018-12-14T18:25:27Z
dc.date.issued2019
dc.identifier.citationJ. 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/3290325en_US
dc.identifier.urihttp://hdl.handle.net/1808/27514
dc.description.abstracten_US
dc.description.abstractWe 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.publisherAssociation for Computing Machineryen_US
dc.rightsThis work is licensed under a Creative Commons Attribution 4.0 International License. © 2019 Copyright held by the owner/author(s).en_US
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en_US
dc.subjectExtensible data typesen_US
dc.subjectRow typesen_US
dc.subjectRow polymorphismen_US
dc.subjectQualified typesen_US
dc.titleAbstracting Extensible Data Types: Or, Rows by Any Other Nameen_US
dc.typeArticleen_US
kusw.kuauthorMorris, J. Garrett
kusw.kudepartmentElectrical Engineering and Computer Scienceen_US
dc.identifier.doi10.1145/3290325en_US
kusw.oaversionScholarly/refereed, author accepted manuscripten_US
kusw.oapolicyThis item meets KU Open Access policy criteria.en_US
dc.rights.accessrightsopenAccessen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

This work is licensed under a Creative Commons Attribution 4.0 International License. © 2019 Copyright held by the owner/author(s).
Except where otherwise noted, this item's license is described as: This work is licensed under a Creative Commons Attribution 4.0 International License. © 2019 Copyright held by the owner/author(s).