Phantom Types and Subtyping
-
jfp06.pdf
(with Riccardo Pucella; To appear in the Journal of Functional Programming)
We investigate a technique from the literature, called the
phantom-types technique, that uses parametric polymorphism, type
constraints, and unification of polymorphic types to model a subtyping
hierarchy. Hindley-Milner type systems, such as the one found in
Standard ML, can be used to enforce the subtyping relation, at least
for first-order values. We show that this technique can be used to
encode any finite subtyping hierarchy (including hierarchies arising
from multiple interface inheritance). We formally demonstrate the
suitability of the phantom-types technique for capturing first-order
subtyping by exhibiting a type-preserving translation from a simple
calculus with bounded polymorphism to a calculus embodying the type
system of SML.
-
arXiv04.pdf
(with Riccardo Pucella; Unpublished; split into the JFP paper above and
the practical datatype specializations paper)
We investigate a technique from the literature, called the phantom
types technique, that uses parametric polymorphism, type constraints,
and unification of polymorphic types to model a subtyping
hierarchy. Hindley-Milner type systems, such as the one found in SML,
can be used to enforce the subtyping relation. We show that this
technique can be used to encode any finite subtyping hierarchy
(including hierarchies arising from multiple interface
inheritance). We formally demonstrate the suitability of the phantom
types technique for capturing subtyping by exhibiting a
type-preserving translation from a simple calculus with bounded
polymorphism to a calculus embodying the type system of SML. We then
illustrate a particular use of the technique to capture programming
invariants associated with user-defined datatypes, in the form of
statically-enforced datatype specializations.
-
tcs02.ps
(with Riccardo Pucella; Appeared at TCS'02;
20020829-TCS02.ppt)
We investigate a technique from the literature, called the phantom
types technique, that uses parametric polymorphism, type constraints,
and unification of polymorphic types to model a subtyping hierarchy.
Hindley-Milner type systems, such as the one found in ML, can be used
to enforce the subtyping relation. We show that this technique can be
used to encode any finite subtyping hierarchy (including hierarchies
arising from multiple interface inheritance). We then formally
demonstrate the suitability of the phantom types technique for
capturing subtyping by exhibiting a type-preserving translation from a
simple calculus with bounded polymorphism to a calculus embodying the
type system of ML.
The documents contained in these directories are included by the
contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a non-commercial basis. Copyright and
all rights therein are maintained by the authors or by other copyright
holders, notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by each
author's copyright. These works may not be reposted without the
explicit permission of the copyright holder.
|
|