Abstract: 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 newtype, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides.
Publication Year: 2007
Publication Date: 2007-01-16
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 238
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot