A proper extension of ML with an effective type-assignment

ABSTRACT

We extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The original definition of ML does not allow this feature. This extension does not produce new types beyond the usual universal polymorphic types of ML and satisfies the properties already enjoyed by ML: the principal-type property and the effective type-assignment property.

REFERENCES

• C: Cardelli, L., "Basic polymorphic typechecking", Polymorphism, Vol. II, No. 1, Jan. 1985.
• CDK: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• CW: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• DM: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• GMW: Gordon, M.J., Milner, R. and Wadsworth, C.P., Edinburgh LCF, LNCS 78, Springer-Verlag, 1979.
• KTU1: Kfoury, A., Tiuryn, J. and Urzyczyn, P., "The hierarchy of finitely typed functional programs", Proc. 2-nd Syrup. on Logic in Computer Science, pp 225- 236, June 1987.
• KTU2: Kfoury, A., Tiuryn, J. and Urzyczyn, P., "A proper extension of ML with an effective typeassignment", unpublished manuscript, July 1987.
• K: Kfoury, A., "An improved polymorphic type discipline", under preparation.
• Mi: Milner, R., "A theory of type polymorphism in programming", J. of Computer and System Sciences, Vol. 17, pp 348-375, 1978.
• My: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• PJ: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Languages