Injective Type Families for Haskell

Jan Stolarek, Simon Peyton Jones, Richard A. Eisenberg

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


Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular type-level programming extension is TypeFamilies, which allows users to write functions on types. Yet, using type functions can cripple type inference in certain situations. In particular, lack of injectivity in type functions means that GHC can never infer an instantiation of a type variable appearing only under type functions. In this paper, we describe a small modification to GHC that allows type functions to be annotated as injective. GHC naturally must check validity of the injectivity annotations. The algorithm to do so is surprisingly subtle. We prove soundness for a simplification of our algorithm, and state and prove a completeness property, though the algorithm is not fully complete. As much of our reasoning surrounds functions defined by a simple pattern-matching structure, we believe our results extend beyond just Haskell. We have implemented our solution on a branch of GHC and plan to make it available to regular users with the next stable release of the compiler.
Original languageEnglish
Title of host publicationProceedings of the 2015 ACM SIGPLAN Symposium on Haskell
Place of PublicationNew York, NY, USA
Number of pages11
ISBN (Print)978-1-4503-3808-0
Publication statusPublished - 2015

Publication series

NameHaskell '15

Fingerprint Dive into the research topics of 'Injective Type Families for Haskell'. Together they form a unique fingerprint.

Cite this