Constrained Type Families
View/ Open
Issue Date
2017-09Author
Morris, J. Garrett
Eisenberg, Richard A.
Publisher
Association for Computing Machinery
Type
Article
Article Version
Scholarly/refereed, publisher version
Rights
© 2017 Copyright held by the owner/author(s). Publication rights licensed to Association for Computing Machinery.
2475-1421/2017/9-ART42.
Metadata
Show full item recordAbstract
We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.
Collections
Citation
J. Garrett Morris and Richard A. Eisenberg. 2017. Constrained Type Families. Proc. ACM Program. Lang. 1,
ICFP, Article 42 (September 2017), 28 pages.
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.