Constrained Type Families

J. Garrett Morris, Richard A. Eisenberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publication22nd ACM SIGPLAN International Conference on Functional Programming.
PublisherACM
Number of pages28
Volume1
DOIs
Publication statusPublished - 29 Aug 2017
Event22nd ACM SIGPLAN International Conference on Functional Programming - Oxford, United Kingdom
Duration: 3 Sep 20179 Sep 2017
https://conf.researchr.org/home/icfp-2017

Publication series

Name
PublisherACM
Volume1
ISSN (Electronic)2475-1421

Conference

Conference22nd ACM SIGPLAN International Conference on Functional Programming
Abbreviated titleICFP 2017
CountryUnited Kingdom
CityOxford
Period3/09/179/09/17
Internet address

Cite this