System F with Type Equality Coercions Export

@article{citeulike:675327, abstract = {We introduce a variant of System F that uses a single mechanism to enable the type preserving translation of generalised abstract data types (GADTs), type classes with associated types and functional dependencies, as well as closed type functions. The core idea is to pass around explicit evidence for type equalities, just like System F passes types explicitly. We use this evidence to justify type casts encoding non-syntactic type equalities induced by the mentioned source language features. In particular, we don't need special typing rules for pattern matching on GADTs, we can easily combine GADTs with type classes, and we can relax restrictions on programs involving associated types or functional dependencies.}, author = {Sulzmann, Martin and Chakravarty, Manuel and Peyton-Jones, Simon}, citeulike-article-id = {675327}, citeulike-linkout-0 = {http://research.microsoft.com/~simonpj/papers/ext-f/}, keywords = {associated-types, gadt, intermediate-language, type-classes, type-equality}, posted-at = {2006-05-30 19:46:16}, priority = {0}, title = {System F with Type Equality Coercions}, url = {http://research.microsoft.com/~simonpj/papers/ext-f/} }

TY - JOUR ID - citeulike:675327 L3 - citeulike-article-id:675327 N2 - We introduce a variant of System F that uses a single mechanism to enable the type preserving translation of generalised abstract data types (GADTs), type classes with associated types and functional dependencies, as well as closed type functions. The core idea is to pass around explicit evidence for type equalities, just like System F passes types explicitly. We use this evidence to justify type casts encoding non-syntactic type equalities induced by the mentioned source language features. In particular, we don't need special typing rules for pattern matching on GADTs, we can easily combine GADTs with type classes, and we can relax restrictions on programs involving associated types or functional dependencies. TI - System F with Type Equality Coercions KW - associated-types KW - gadt KW - intermediate-language KW - type-classes KW - type-equality AU - Sulzmann, Martin AU - Chakravarty, Manuel AU - Peyton-Jones, Simon UR - http://research.microsoft.com/~simonpj/papers/ext-f/ ER -