Abstract
It has been long argued that the well known Milner type inference system implemented in the programming language Standard ML is inadequate [4]. The arguments were presented on the basis of intersection-type inference systems [3]. However no algorithm has been developed. The intersection-type inference systems are closed underβ-equality [1] and has been proved undecidable [7]. The paper presents a new type inference system using conjunction-types which extends the notion of intersection-types. The algorithm presented in the author's previous paper [9] is easily adoptable into the Standard ML. In this paper we shall discuss the features of the system and its semantic soundness. Unlike the intersection-type inference systems, the conjunction-type inference system is:
-
1.
decidable
-
2.
semantically sound for all types
-
3.
semantically sound and complete for basic types.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Bakel, Steffen van. Derivations In Type Assignment Systems.Thesis, University of Nijmegen, The Netherlands, (1988).
Barendregt, H. The Lambda Calculus. Its Syntax and Semantics.ISBN 0-444-87508-5, North-Holland Publishing Company, (1981).
Barendregt, H. et al. A Filter Lambda Model And The Completeness of Type Assignment.Journal of Symbolic Logic 48(4, December (1985).
Coppo, M. An Extended Polymorphic Type System For Applicative Languages.Lecture Notes in Computer Science 88, Rydzyna, Poland, September (1980).
Courcelle, B. Fundamental Properties Of Infinite Trees.Theoretical Computer Science 25(95–169, (1983).
Damas, L. M. M. Type Assignment in Programming Languages.CST-33-85, Department of Computer Science, University of Edinburgh, Scotland, April (1985).
Dirven, A. P. M. Composition Of A New Type Assignment Algorithm, using Turino Conjunctions of Curry Types.Thesis, University of Nijmegen, The Netherlands, (1988).
Ghosh-Roy, R. Conjunctional Polymorphism.Proceedings, The Tenth Australian Computer Science Conference, Australia, (1987).
Ghosh-Roy, R., et al. Conjunctional Polymorphism in Programming Languages.Proceedings, The ACM Computer Science Conference, Georgia, USA, February (1988).
Ghosh-Roy, R. Conjunction Type Standard ML Polymorphism.Abstract, The ACM Computer Science Conference, Washington, D.C., USA, February (1990).
MacQueen, D., et al. An Ideal Model for Recursive Polymorphic Types.Information and Control 71(95–130), (1986).
Milner, R. A Theory of Type Polymorphism in Programming.CSR-9-77, University of Edinburgh, Department of Computer Science, (1977).
Reynolds, J. C. Three Approaches to Type Structure.Lecture Notes in Computer Science 185(97–138, (1985).
Robinson, J.A. A Machine Oriented Logic Based on The Resolution Principle.Journal of The Association for Computing Machinery 12, (1965).
Rocca, S. R. D. Principal Type Scheme and Unification for Intersection Type Discipline.Internal Report, Dipartimento di Informatica — Universitdi Torino, Torino, Italy, (1988).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Ghosh-Roy, R. Conjunction-type standard ML polymorphism. Lisp and Symbolic Computation 3, 381–409 (1990). https://doi.org/10.1007/BF01807698
Issue Date:
DOI: https://doi.org/10.1007/BF01807698