Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Blume. No-Longer-Foreign: Teaching an ML compiler to speak C “natively”. In Electronic Notes in Theoretical Computer Science, volume 59. Elsevier Science Publishers, 2001.
E Burton. Type extension through polymorphism. ACM Transactions on Programming Languages and Systems, 12 (1): 135–138, January 1990.
L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov. An extension of System F with subtyping. Information and Computation, 109 (1–2): 4–56, 1994.
L. Damas and R. Milner. Principal type-schemes for functional programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, pages 207–212. ACM Press, 1982.
C. Elliott, S. Finne, and O. de Moor. Compiling embedded languages. In Workshop on Semantics, Applications, and Implementation of Program Generation, 2000.
S. Finne, D. Leijen, E. Meijer, and S. Peyton Jones. Calling hell from heaven and heaven from hell. In Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, pages 114–125. ACM Press, 1999.
S. Kahrs. Red-black trees with types. Journal of Functional Programming, 11 (3): 425–432, 2001.
D. Leijen and E. Meijer. Domain specific embedded compilers. In Proceedings of the Second Conference on Domain-Specific Languages (DSL’99), pages 109–122, 1999.
R. Milner. A theory of type polymorphism in programming. Journal of Computer and Systems Sciences, 17 (3): 348–375, 1978.
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Mass., 1997.
F. Pessaux and X. Leroy. Type-based analysis of uncaught exceptions. In Conference Record of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 276–290. ACM Press, 1999.
D. Rémy. Records and variants as a natural extension of ML. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, pages 77–88. ACM Press, 1989.
J. H. Reppy. A safe interface to sockets. Technical memorandum, AT&T Bell Laboratories, 1996.
M. Wand. Complete type inference for simple objects. In Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media New York
About this chapter
Cite this chapter
Fluet, M., Pucella, R. (2002). Phantom Types and Subtyping. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds) Foundations of Information Technology in the Era of Network and Mobile Computing. IFIP — The International Federation for Information Processing, vol 96. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35608-2_37
Download citation
DOI: https://doi.org/10.1007/978-0-387-35608-2_37
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5275-5
Online ISBN: 978-0-387-35608-2
eBook Packages: Springer Book Archive