Declaration-free type checking

ABSTRACT

Conventional Milner-style polymorphic type checkers automatically infer types of functions and simple composite objects such as tuples. Types of recursive data structures (e.g. lists) have to be defined by the programmer through an abstract data type definition. In this paper, we show how abstract data types, involving type union and recursion, can be automatically inferred by a type checker. The language for describing such types is that of regular trees, a generalization of regular expressions to denote sets of tree structured terms. Inference of these types is reducible to the problem of solving simultaneous inclusion inequations over regular trees. We present algorithms to solve such inequations. Using these techniques, programs without any type definitions and type annotations for functions can be type checked.

REFERENCES

• 1: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 2: 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
• 3: W. F. Clocksin , C. S. Mellish, Programming in Prolog, Springer-Verlag New York, Inc., New York, NY, 1987
• 4: 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]
• 5: [5] Despeyroux, T. Executable specifications of static semantaics. In Lecture Notes in Comp. Sci. Volume 173: Semantics of Data Types, Springer-Verlag, 1984, pp. 215-233.
• 6: K Jensen , N Wirth , A B Mickel , J F Miner, Pascal user manual and report; 3rd ed., Springer-Verlag New York, Inc., New York, NY, 1985
• 7: Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582161]
• 8: [8] Keller, R. M. FEL (Function Equation Language) Programmer's Guide. AMPS Technical Memorandum 7, University of Utah, April, 1982.
• 9: D. B. MacQueen , Ravi Sethi, A semantic model of types for applicative languages, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.243-252, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802156]
• 10: [10] Milner, R. A theory of type polymorphism in programming. J. Computer and System Sciences 17 (1978), pp. 348-375.
• 11: Robin Milner, A proposal for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.184-197, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802035]
• 12: [12] Mishra, P. Data types in applicative languages: abstraction and inference. University of Utah, 1983.
• 13: [13] Mishra, P. Towards a theory of types in Prolog. International symposium on logic programming. IEEE, 1984, pp. 289-298.
• 14: 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]
• 15: 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
• 16: [16] Reddy, U. S. On the relationship between logic and functional languages. In DeGrot. D, Lindstrom, G., Eds., Functional and Logic Programming. Prentice-Hall, 1985.
• 17: [17] Reynolds R. C. Automatic Computation of Data Set Definitions. IFIP 68, 1968, pp. 456-461.
• 18: Adi Shamir , William W. Wadge, Data Types as Objects, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.465-479, July 18-22, 1977
• 19: [19] Thatcher, J. W. Tree automata: an informal survey. In A. V. Aho, Ed., Currents in theory of computing, Prentice-Hall, 1973, pp. 143-172.
• 20: [20] Turner, D. A. SASL Language Manual. St. Andrews University, 1976.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

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

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Design, Languages, Performance, Theory

Keywords:
equational languages, regular trees, solving inequations, type inference