Phantom Types,James Cheney,Ralf Hinze

Phantom Types   (Citations: 10)
BibTex | RIS | RefWorks Download
Phantom types are data types with type constraints asso- ciated with dierent cases. Examples of 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 equa- tions between type constructors as well as type functions of higher-order kinds. We prove type soundness and decidability for a Haskell-like lan- guage extended by phantom types.
Cumulative Annual
    • ...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 type-checker 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 Sheardet al. Meta-programming With Built-in 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. Licataet al. Dependently Typed Programming with Domain-Specific 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 Chenet 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

Sort by: