Closed Type Families with Overlapping Equations

  • Richard A. Eisenberg ,
  • Dimitrios Vytiniotis ,
  • Simon Peyton Jones ,
  • Stephanie Weirich

Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |

Published by ACM

Publication

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.

Here is an extended version with proofs.