TLDI 2007 START Conference Manager    

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


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.

START Conference Manager (V2.53.7)