System F with Type Equality Coercions
Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jones and Kevin Donnelly
The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2007)
Nice, France, January 16, 2007
Abstract
We introduce System FC(X), which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric type functions, given meaning by top-level equality axioms. Unlike System F, FC(X) is expressive enough to serve as a target for several different source-language features, including Haskell's newtype, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides. FC(X) can therefore serve as a typed intermediate language in a compiler that supports these features.