Promoting Functions to Type Families in Haskell

Richard A. Eisenberg, Jan Stolarek

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


Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement.

We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.
Original languageEnglish
Title of host publicationProceedings of the 2014 ACM SIGPLAN Symposium on Haskell
Place of PublicationNew York, NY, USA
Number of pages12
ISBN (Print)978-1-4503-3041-1
Publication statusPublished - 2014

Publication series

NameHaskell '14

Fingerprint Dive into the research topics of 'Promoting Functions to Type Families in Haskell'. Together they form a unique fingerprint.

Cite this