KUKU

KU ScholarWorks

  • myKU
  • Email
  • Enroll & Pay
  • KU Directory
    • Login
    View Item 
    •   KU ScholarWorks
    • Engineering
    • Electrical Engineering and Computer Science Scholarly Works
    • View Item
    •   KU ScholarWorks
    • Engineering
    • Electrical Engineering and Computer Science Scholarly Works
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Constrained Type Families

    Thumbnail
    View/Open
    morris-icfp2017-families.pdf (338.6Kb)
    Issue Date
    2017-09
    Author
    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 record
    Abstract
    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.
    URI
    http://hdl.handle.net/1808/25014
    DOI
    https://doi.org/10.1145/3110286
    Collections
    • Electrical Engineering and Computer Science Scholarly Works [301]
    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.


    Contact KU ScholarWorks
    785-864-8983
    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    785-864-8983

    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    Image Credits
     

     

    Browse

    All of KU ScholarWorksCommunities & CollectionsThis Collection

    My Account

    LoginRegister

    Statistics

    View Usage Statistics

    Contact KU ScholarWorks
    785-864-8983
    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    785-864-8983

    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    Image Credits
     

     

    The University of Kansas
      Contact KU ScholarWorks
    Lawrence, KS | Maps
     
    • Academics
    • Admission
    • Alumni
    • Athletics
    • Campuses
    • Giving
    • Jobs

    The University of Kansas prohibits discrimination on the basis of race, color, ethnicity, religion, sex, national origin, age, ancestry, disability, status as a veteran, sexual orientation, marital status, parental status, gender identity, gender expression and genetic information in the University’s programs and activities. The following person has been designated to handle inquiries regarding the non-discrimination policies: Director of the Office of Institutional Opportunity and Access, IOA@ku.edu, 1246 W. Campus Road, Room 153A, Lawrence, KS, 66045, (785)864-6414, 711 TTY.

     Contact KU
    Lawrence, KS | Maps