Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(6)
Data Type
Dynamic Typing
Generating Function
Higher Order Abstract Syntax
Standard Ml
Higher Order
Related Publications
(5)
Cayenne  A Language with Dependent Types
Typing dynamic typing
Guarded recursive datatype constructors
A lightweight implementation of generics and dynamics
An extension of HM(X) with bounded existential and universal datatypes
Subscribe
Academic
Publications
Phantom Types
Phantom Types,James Cheney,Ralf Hinze
Edit
Phantom Types
(
Citations: 10
)
BibTex

RIS

RefWorks
Download
James Cheney
,
Ralf Hinze
Phantom types are data types with type constraints asso ciated with dierent cases. Examples of phantom types include typed type representations and typed higherorder
abstract syntax
trees. These types can be used to support typed generic functions, dynamic typing, and staged compilation in higherorder, statically typed languages such as Haskell or Standard ML. In our system, type constraints can be equa tions between type constructors as well as type functions of higherorder kinds. We prove type soundness and decidability for a Haskelllike lan guage extended by phantom types.
Cumulative
Annual
Citation Context
(6)
...These sometimes irreconcilable goals are made possible by embedding the mega logic in a type system based on equality qualified types[
6
]...
...While this can be done using only the standard extensions to the Haskell 98 type system (using equality types), we use mega, an extension to Haskell inspired by Cheney and Hinze’s work on phantom types [
6
]...
...The technique of encoding the equality between types a and b as a polymorphic function of type 8’. (’ a)!(’ b) was proposed by both Baars & Swierstra [2], and Cheney & Hinze [
6
] at about the same time, and is described somewhat earlier in a dierent setting by Weirich [ 20]...
...What if we could extend the type system of Haskell, in a relatively minor way, to allow the typechecker itself to manipulate and propagate equality proofs? Such a type system was proposed by Cheney and Hinze [
6
], and is one of the ideas behind mega [ 17]...
...Hinze and Cheney [5,
6
] have recently resurrected the notion of “phantom type,” first introduced by Leijen and Meijer [10]...
Tim Sheard
,
et al.
Metaprogramming With Builtin Type Equality
...There has been a great deal of work on integrating various forms of dependent types into practical programming languages and their implementations [3, 7,
9
, 10, 11, 15, 19, 20, 37, 39, 42, 44, 52, 53, 55, 59, 60, 61, 64], building on dependently typed proof assistants such as NuPRL [12] and Coq [6]...
Daniel R. Licata
,
et al.
Dependently Typed Programming with DomainSpecific Logics
...These sometimes irreconcilable goals are made possible by embedding the Ωmega logic in a type system based on equality qualified types[
7
]...
...The ability to combine type inference with type checking and arbitrary rank polymorhism[12, 14, 27]; the semantics of staged computation systems[5, 32, 26, 30]; and the use of simplified form of depen dent typing called indexed types[44, 6,
7
] have combined to create a powerful new way to embed properties of programs in their types...
...Equality constrained types are a relatively new feature in t he world of programming languages, and were only recently introduced by Hinze and Cheney[
7
]...
...Using type equality became practical with the introduction of equalit y qualified types by Hinze and Cheney[
7
]...
Tim Sheard
.
Languages of the future
...Only recently is the need for type equality elimination functions identified [
5
]...
...Of course, this simple approach does not address at all the diculty in constructing proof terms, for which we may need to introduce guarded datatypes [19] or phantom types [
5
] into Haskell...
Chiyan Chen
,
et al.
Implementing Cut Elimination: A Case Study of Simulating Dependent Typ...
...The sometimes irreconcilable goals of being both a programming language and a logic, are made possible by embedding the Ωmega logic in a type system based on equality qualified types[
9
]...
...Equality qualified types are a relatively new feature in the world of programming languages, and were only recently introduced by Hinze and Cheney[
9
]...
...Ωmega’s design has been influenced by work on Logical Frameworks[16, 30, 29], Inductive Families[14, 10], Refinement Types[15, 12], Practical Dependent Typing[1, 2], and Guarded Recursive Datatype Constructors[52, 8]. But the work on Equality Types[
9
] has allowed us to express many of these ideas as a simple extension (based upon qualified types) to the familiar notion of Algebraic Datatypes...
...Using type equality became practical with the introduction of equality qualified types by Hinze and Cheney[
9
]...
Tim Sheard
.
Languages of the future
References
(26)
Dynamic Typing in Polymorphic Languages
(
Citations: 91
)
Martín Abadi
,
Luca Cardelli
,
Benjamin C. Pierce
,
Didier Rémy
Journal:
Journal of Functional Programming  JFP
, vol. 5, no. 1, pp. 111130, 1995
Cayenne  A Language with Dependent Types
(
Citations: 205
)
Lennart Augustsson
Conference:
International Conference on Functional Programming  ICFP
, vol. 1608, pp. 240267, 1998
Typing dynamic typing
(
Citations: 58
)
Arthur I. Baars
,
S. Doaitse Swierstra
Journal:
Sigplan Notices  SIGPLAN
, vol. 37, no. 9, pp. 157166, 2002
Nested Datatypes
(
Citations: 89
)
Richard S. Bird
,
Lambert G. L. T. Meertens
Conference:
Mathematics of Program Construction  MPC
, pp. 5267, 1998
A lightweight implementation of generics and dynamics
(
Citations: 71
)
James Cheney
,
Ralf Hinze
Conference:
haskell workshop
, pp. 90104, 2002
Sort by:
Citations
(10)
Metaprogramming With Builtin Type Equality
(
Citations: 36
)
Tim Sheard
,
Emir Pasalic
Journal:
Electronic Notes in Theoretical Computer Science  ENTCS
, vol. 199, pp. 4965, 2008
Dependently Typed Programming with DomainSpecific Logics
(
Citations: 2
)
Daniel R. Licata
,
Robert Harper
Published in 2008.
Combining programming with theorem proving
(
Citations: 74
)
Chiyan Chen
,
Hongwei Xi
Journal:
Sigplan Notices  SIGPLAN
, vol. 40, no. 9, pp. 6677, 2005
Languages of the future
(
Citations: 79
)
Tim Sheard
Journal:
Sigplan Notices  SIGPLAN
, vol. 39, no. 12, pp. 116119, 2004
Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell
(
Citations: 15
)
Chiyan Chen
,
Dengping Zhu
,
Hongwei Xi
Conference:
Practical Aspects of Declarative Languages  PADL
, pp. 239254, 2004