Abstract
This paper describes a simple extension of the Hindley-Milner polymorphic type discipline to call-by-value languages that incorporate imperative features like references, exceptions, and continuations. This extension sacrifices the ability to type every purely functional expression that is typable in the Hindley-Milner system. In return, it assigns the same type to functional and imperative implementations of the same abstraction. Hence with a module system that separates specifications from implementations, imperative features can be freely used to implement polymorphic specifications. A study of a number of ML programs shows that the inability to type all Hindley-Milner typable expressions seldom impacts realistic programs. Furthermore, most programs that are rendered untypable by the new system can be easily repaired.
Similar content being viewed by others
References
“Standard ML of New Jersey release notes (version 0.93),” AT&T Bell Laboratories (November 1993).
Damas, L. M. M.Principal Type Schemes for Functional Programs, InProceedings of the 9th Annual ACM Symposium on Principles of Programming Languages (January 1982) 207–212.
Damas, L. M. M.Type Assignment in Programming Languages, PhD thesis, University of Edinburgh (1985).
Greiner, J. “Standard ML weak polymorphism can be sound,” Technical Report CMU-CS-93-160R, Carnegie Mellon University (September 1993).
Harper, R. and M. Lillibridge. “Explicit polymorphism and CPS conversion,” InConference Record of the 20th Annual ACM Symposium on Principles of Programming Languages (January 1993) 206–219.
Harper, R., B. F. Duba, and D. MacQueen. “Typing first-class continuations in ML,”Journal of Functional Programming 3, 4 (October 1993), 465–484.
Hindley, R. “The principal type-scheme of an object in combinatory logic,”Transactions of the American Mathematical Society, 146 (December 1969) 29–60.
Hoang, M., J. Mitchell, and R. Viswanathan. “Standard ML-NJ weak polymorphism and imperative constructs,” InProceedings of the Eighth Annual Symposium on Logic in Computer Science (June 1993) 15–25.
Leroy, X.Typage polymorphe d'un langage algorithmique, PhD thesis, L'Université Paris 7 (1992).
Leroy, X. “Polymorphism by name for references and continuations,” InConference Record of the 20th Annual ACM Symposium on Principles of Programming Languages (January 1993) 220–231.
Leroy, X. and P. Weis. “Polymorphic type inference and assignment,” InProceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991) 291–302.
Milner, R. “A theory of type polymorphism in programming,”Journal of Computer and System Sciences, 17 (1978) 348–375.
Milner, R. and M. Tofte.Commentary on Standard ML, MIT Press, Cambridge, Massachusetts (1991).
Milner, R., M. Tofte, and R. Harper.The Definition of Standard ML, MIT Press, Cambridge, Massachusetts (1990).
Ohori, A. “A simple semantics for ML polymorphism,” InProceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (September 1989) 281–292.
Reppy, J. H.Higher-order Concurrency, PhD thesis, Cornell University (1991).
Talpin, J.-P. and P. Jouvelot. “The type and effect discipline,” InProceedings of the Seventh Annual Symposium on Logic in Computer Science (June 1992) 162–173.
Tofte, M. “Type inference for polymorphic references,”Information and Computation, 89, 1 (November 1990) 1–34.
Wright, A. K. “Typing references by effect inference,” InProceedings of the 4th European Symposium on Programming, Springer-Verlag Lecture Notes in Computer Science 582 (1992) 473–491.
Wright, A. K. and M. Felleisen. “A Syntactic Approach to Type Soundness,” Technical Report 91–160, Rice University (April 1991). To appear inInformation and Computation, 1994.
Author information
Authors and Affiliations
Additional information
This research was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship.
Rights and permissions
About this article
Cite this article
Wright, A.K. Simple imperative polymorphism. LISP and Symbolic Computation 8, 343–355 (1995). https://doi.org/10.1007/BF01018828
Issue Date:
DOI: https://doi.org/10.1007/BF01018828