Partial type inference for untyped functional programs

ABSTRACT

This extended abstract describes a way of inferring as much type information as possible about programs written in an untyped programming language. We present an algorithm that underlines the untypable parts of a program and assigns types to the rest. The algorithm is derived in a very simple manner from the well-known algorithm W of Damas & Milner [Damas and Milner 1982]. Our algorithm provides us with an easy solution to the problem of doing binding time analysis of the untyped higher order lambda calculus, and thereby of the wide range of programming languages based upon the lambda calculus. The techniques can also be used to eliminate superfluous runtime type checking in untyped functional languages, to produce better error messages from type analyzers for strongly typed languages, and to analyze feasibility of arity raising.

REFERENCES

• Bondorf 1990: A. Bondorf, Automatic autoprojection of higher order recursive equations, Proceedings of the third European symposium on programming on ESOP '90, p.70-87, May 1990, Copenhagen, Denmark
• Bondorf et al. 1988: A. Bondorf, N.D. Jones, T. Mogensen, and P. Sestoft, Binding Time Analysis and the Taming o/Sell-Application, Draft, 18 pages, DIKU, University of Copenhagen, Denmark, August 1988.
• Damas and Milner 1982: 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]
• Fuh and Mishra 1989: You-Chin Fuh , Prateek Mishra, Polymorphic Subtype Inference: Closing the Theory-Practice Gap, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.167-183, March 13-17, 1989
• Gomard 1989: C. K. Gomard, Higher Order Partial Evaluation - HOPE/or the Lambda Calculus, Master's thesis, DIKU, University of Copenhagen, Denmark, September 1989.
• Jones et al. 1989: N.D. Jones, P. Sestoft, and H. S0ndergaard, Mix: A Self-Applicable Partial Evaluator for Experiments in Compiler Generation, Lisp and Symbolic Computation 2,1 (1989) 9-50.
• Jones et al. 1990: N.D. Jones, C.K. Gomard, A. Bondorf, O. Danvy, and T.~. Mogensen, A Self-Applicable Partial Evaluator for the Lambda Calculus, in 1990 International Con/erence on Computer Languages, New Orleans, Louisiana, March 1990, IEEE Computer Society, 1990. To appear.
• Kuo and Mishra 1989: Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
• Mogensen 1989: Torben Æ. Mogensen, Binding Time Analysis for Polymorphically Typed Higher Order Languages, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.298-312, March 13-17, 1989
• Nielson and Nielson 1988: H. R. Nielson , F. Nielson, Automatic binding time analysis for a typed &lgr;-calculus, Science of Computer Programming, v.10 n.2, p.139-176, April 1988 [doi>10.1016/0167-6423(88)90025-1]
• Robinson 1965: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• Romanenko 1990: S. A. Romanenko, Arity raiser and use in program specialization, Proceedings of the third European symposium on programming on ESOP '90, p.341-360, May 1990, Copenhagen, Denmark
• Schmidt 1988: D.A. Schmidt, Static Properties of Partial Evaluation, in Partial Evaluation and Mixed Computation, edited by D. Bj0rner, A.P. Ershov, and N.D. Jones, pp. 465-483, North-Holland, 1988.
• Wadler 1990: P. Wadler, Linear Types Can Change the World!, in Programming Concepts and Methods iFIP TC~, 1990. (to appear).
• Wand 1986: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]

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.2 Language Classifications
          Subjects: Applicative (functional) languages

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages