Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. First-Class Phantom Types

First-Class Phantom Types

File(s)
TR2003-1901.pdf (352.86 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5614
Collections
Computing and Information Science Technical Reports
Author
Cheney, James
Hinze, Ralf
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.

Date Issued
2003-07-10
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance