ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
Partial type constructors: Or, making ad hoc datatypes less ad hoc
dc.contributor.author | Jones, Mark P. | |
dc.contributor.author | Morris, J. Garrett | |
dc.contributor.author | Eisenberg, Richard A. | |
dc.date.accessioned | 2021-02-09T20:20:15Z | |
dc.date.available | 2021-02-09T20:20:15Z | |
dc.date.issued | 2020-01 | |
dc.identifier.citation | Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg. 2019. Partial type constructors: or, making ad hoc datatypes less ad hoc. Proc. ACM Program. Lang. 4, POPL, Article 40 (January 2020), 28 pages. DOI:https://doi.org/10.1145/3371108 | en_US |
dc.identifier.uri | http://hdl.handle.net/1808/31400 | |
dc.description | This work is licensed under a Creative Commons Attribution 4.0 International License. | en_US |
dc.description.abstract | Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code. | en_US |
dc.publisher | Association for Computing Machinery (ACM) | en_US |
dc.rights | Copyright © 2019 Owner/Author. | en_US |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | en_US |
dc.subject | Theory of computation | en_US |
dc.subject | Software and its engineering | en_US |
dc.subject | Data types and structures | en_US |
dc.subject | Type constructors | en_US |
dc.subject | Parametric polymorphism | en_US |
dc.title | Partial type constructors: Or, making ad hoc datatypes less ad hoc | en_US |
dc.type | Article | en_US |
kusw.kuauthor | Morris, J. Garrett | |
kusw.kudepartment | Electrical Engineering & Computer Science | en_US |
dc.identifier.doi | 10.1145/3371108 | en_US |
kusw.oaversion | Scholarly/refereed, publisher version | en_US |
kusw.oapolicy | This item meets KU Open Access policy criteria. | en_US |
dc.rights.accessrights | openAccess | en_US |