Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Research Papers of Manuel Chakravarty
[go: Go Back, main page]

System F with Type Equality Coercions

Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. In G. Necula, editor, Proceedings of The Third ACM SIGPLAN Workshop on Types in Language Design and Implementation, ACM Press, 2007. (An extended version appeared as Technical Report UNSW-CSE-TR-0624, 2006.)

*new*

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.

PDF, conference version (14 pages)
PDF, TR version (19 pages)

This page is part of Manuel Chakravarty's WWW-stuff.