Abstract
The ML type system was originally introduced as a means of identifying a class of terms in a simple untyped language, often referred to as core-ML, whose evaluation could be guaranteed not to “go wrong”. In subsequent work, the terms of core-ML have also been viewed as a ‘convenient shorthand’ for programs in typed languages. Notable examples include studies of ML polymorphism and investigations of overloading, motivated by the use of type classes in Haskell.
In this paper, we show how qualified types, originally developed to study type class overloading, can be used to explore the relationship between core-ML programs and their translations in an explicitly typed language. Viewing these two distinct applications as instances of a single framework has obvious advantages; many of the results that have been established for one can also be applied to the other.
We concentrate particularly on the issue of coherence, establishing sufficient conditions to guarantee that all possible translations of a given core-ML term are equivalent. One of the key features of this work is the use of conversions, similar to Mitchell's retyping functions, to provide an interpretation of the ordering between type schemes in the target language.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S.M. Blott. An approach to overloading with polymorphism. Ph.D. thesis, Department of computing science, University of Glasgow, July 1991 (draft version).
V. Breazu-Tannen, T. Coquand, C.A. Gunter and A. Scedrov. Inheritance and coercion. In IEEE Symposium on Logic in Computer Science, 1989.
P.-L. Curien and G. Ghelli. Coherence of subsumption. In Fifteenth Colloquium on Trees in Algebra and Programming. Springer Verlag LNCS 431, 1990.
L. Damas and R. Milner. Principal type schemes for functional programs. In 8th Annual ACM Symposium on Principles of Programming languages, 1982.
R. Harper and J.C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15, 2, April 1993.
B. Hilken and D. Rhydeheard. Towards a categorical semantics of type classes. In Theoretical aspects of computer software. Springer Verlag LNCS 526, 1991.
J.R. Hindley and J.P. Seldin. Introduction to combinators and λ-calculus. London mathematical society student texts 1. Cambridge University Press, 1986.
P. Hudak, S.L. Peyton Jones and P. Wadler (eds.). Report on the programming language Haskell, version 1.2. A CM SIGPLAN notices, 27, 5, May 1992.
M.P. Jones. A theory of qualified types. In European symposium on programming. Springer Verlag LNCS 582, 1992.
M.P. Jones. Qualified types: Theory and Practice. D. Phil. Thesis. Programming Research Group, Oxford University Computing Laboratory. July 1992.
M.P. Jones. From polymorphism to monomorphism by partial evaluation. Yale University, Department of Computer Science. Submitted for publication, July 1993.
S. Kaes. Type inference in the presence of overloading, subtyping and recursive types. In ACM Conference on LISP and functional programming San Francisco, California, June 1992.
X. Leroy. Polymorphism by name for references and continuations. In 20th Annual Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17, 3, 1978.
R. Milner, M. Tofte and R. Harper. The definition of Standard ML. The MIT Press, 1990.
J.C. Mitchell, Polymorphic type inference and containment. In G. Huet (ed.), Logical Foundations of Functional Programming, Addison Wesley, 1990.
T. Nipkow and G. Snelting. Type classes and overloading resolution via ordersorted unification. In 5th ACM conference on Functional Programming Languages and Computer Architecture, Cambridge, MA, August 1991. Lecture notes in computer science 523, Springer Verlag.
T. Nipkow and C. Prehofer. Type checking type classes. In 20th Annual Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.
A. Ohori. A simple semantics for ML polymorphism. In 4th International Conference on Functional Programming Languages and Computer Architecture, Imperial College, London, September 1989. ACM Press.
J.C. Reynolds. The coherence of languages with intersection types. In Theoretical aspects of computer software. Springer Verlag LNCS 526, 1991.
G. Smith. Polymorphic type inference for languages with overloading and subtyping. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York. August 1991.
S. Thatte. Type inference and implicit scaling. In European Symposium on Programming. Springer Verlag LNCS 432, 1990.
S. Thatte. Typechecking with ad hoc polymorphism.Manuscript, Department of mathematics and computer science, Clarkson University, Potsdam, NY. May 1992.
D. Volpano and G. Smith. On the complexity of ML typability with overloading. In 5th A CM conference on Functional Programming Languages and Computer Architecture. Lecture notes in computer science 523. Springer Verlag. 1991.
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In ACM Principles of Programming Languages, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, M.P. (1994). ML typing, explicit polymorphism and qualified types. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_90
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_90
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive