Skip to main content


eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: First-Class Phantom Types
Authors: Cheney, James
Hinze, Ralf
Keywords: computer science
technical report
Issue Date: 10-Jul-2003
Publisher: Cornell University
Abstract: Classical phantom types are datatypes in which type constraints are expressed using type variables that do not appear in the datatype cases themselves. They can be used to embed typed languages into Haskell or ML. However, while such encodings guarantee that only well-formed data can be constructed, they do not permit type-safe deconstruction without additional tagging and run-time checks. We introduce first-class phantom types, which make such constraints explicit via type equations. Examples of first-class phantom types include typed type representations and typed higher-order abstract syntax trees. These types can be used to support typed generic functions, dynamic typing, and staged compilation in higher-order, statically typed languages such as Haskell or Standard ML. In our system, type constraints can be equations between type constructors as well as type functions of higher-order kinds. We prove type soundness and decidability for a Haskell-like language extended by first-class phantom types.
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
TR2003-1901.pdf352.86 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us