Type inference with subtypes

ABSTRACT

We give an algorithm for type inference in a language with functions, records, and variant records. A similar language was studied by Cardelli who gave a type checking algorithm. This language is interesting because it captures aspects of object-oriented programming using subtype polymorphism. We give a type system for deriving types of expressions in the language and prove the type inference algorithm is sound, i.e., it returns a type derivable from the proof system. We also prove that the type the algorithm finds is a “principal” type, i.e., one which characterizes all others. The approach taken here is due to Milner for universal polymorphism. The result is a synthesis of subtype polymorphism and universal polymorphism.

REFERENCES

• 1: Hassan Aït-Kaci , Roger Nasr, Logic and inheritance, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.219-228, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512664]
• 2: H Aït-Kaci , R Nasr, Login: A logic programming language with built-in inheritance, Journal of Logic Programming, v.3 n.3, p.185-215, Oct. 1986 [doi>10.1016/0743-1066(86)90013-0]
• 3: Boehm, Hans-Juergen. "Partial Polymorphic Type In~erence is Undecidable." Proceedings of the 26th Symposium of Foundations of Computer Sc/ence, 1985, pages 339-345.
• 4: Hans-Juergen Boehm , Alan Demers, Implementing RUSSELL, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.186-195, June 25-27, 1986, Palo Alto, California, United States
• 5: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 6: Cardelli, Luca. "Basic po|ymorphi~ typechecking." Polymorphism: The ML//LCF//HOPE Newsletter, volume 2, number 1, january 1985.
• 7: 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]
• 8: tIindley, Roger :lames. "The principal type-scheme of an object in combinatory logic." Transactions of the American Mathematical Society, "~olume 146, December 1969, pages 29-60.
• 9: Milner, Robin. "A theory of type polymorphism in programming." Journal of Computer and System Science, volume 17, number 3, 1978, pages 348-375.
• 10: Milner, Robin. "The standard ML core language (revised)." Polymorph/sm: The ML/LCF/Hope Newsletter, volume 2, number 2, October 1985. (Also Edinburgh report ECS-LFCS-86-2, March 1986.)
• 11: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• 12: Wand, Mitchell. "Complete type inference for simple objects." In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, 1987, pages 37-44.

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.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Algorithms, Languages