We introduce System FC, 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 is expressive enough to serve as a target for several different source-language features, including Haskell's
algebraic data types, associated types, functional dependencies, and
perhaps more besides.
PDF, conference version (14 pages)
PDF, TR version (19 pages)
This page is part of Manuel Chakravarty's WWW-stuff.