Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

ABSTRACT

System E is a recently designed type system for the λ-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution.This paper uses expansion variables in a unification-based automatic type inference algorithm for System~E that succeeds for every β-normalizable λ-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one β-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and β-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.

REFERENCES

• 1: Anindya Banerjee, A modular, polyvariant and type-based closure analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.1-10, June 09-11, 1997, Amsterdam, The Netherlands
• 2: H. Barendregt, M. Coppo, M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4), 1983.
• 3: H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.
• 4: G. Boudol, P. Zimmer. On type inference in the intersection type discipline. Draft available from 1st author's web page, 2004.
• 5: S. Carlier, J. Polakow. System E experimentation tool. http://www.macs.hw.ac.uk/ultra/compositional-analysis/system-E.
• 6: S. Carlier, J. Polakow, J. B. Wells, A. J. Kfoury. System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In Programming Languages & Systems, 13th European Symp. Programming, vol. 2986 of LNCS. Springer-Verlag, 2004.
• 7: Mario Coppo , Ferruccio Damiani , Paola Giannini, Strictness, totality, and non-standard-type inference, Theoretical Computer Science, v.272 n.1-2, p.69-112, February 6, 2002 [doi>10.1016/S0304-3975(00)00348-0]
• 8: M. Coppo, M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4), 1980.
• 9: M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Principal type schemes and λ-calculus semantics. In Hindley and Seldin {17}.
• 10: Ferruccio Damiani, A conjunctive type system for useless-code elimination, Mathematical Structures in Computer Science, v.13 n.1, p.157-197, February 2003 [doi>10.1017/S0960129502003869]
• 11: Ferruccio Damiani, Rank 2 intersection types for local definitions and conditional expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.4, p.401-451, July 2003 [doi>10.1145/778559.778560]
• 12: Ferruccio Damiani, Rank 2 intersection types for modules, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.67-78, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888259]
• 13: Ferruccio Damiani , Paola Giannini, Automatic useless-code elimination for HOT functional programs, Journal of Functional Programming, v.10 n.6, p.509-559, November 2000 [doi>10.1017/S0956796800003786]
• 14: Jean-Yves Girard, Linear logic: its syntax and semantics, Proceedings of the workshop on Advances in linear logic, p.1-42, June 1995
• 15: C. Haack, J. B. Wells. Type error slicing in implicitly-typed higher-order languages. In Programming Languages & Systems, 12th European Symp. Programming, vol. 2618 of LNCS. Springer-Verlag, 2003. Superseded by {16}.
• 16: Christian Haack , J. B. Wells, Type error slicing in implicitly typed higher-order languages, Science of Computer Programming, v.50 n.1-3, p.189-224, March 2004 [doi>10.1016/j.scico.2004.01.004]
• 17: J. R. Hindley, J. P. Seldin, eds. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
• 18: Thomas P. Jensen, Inference of polymorphic and conditional strictness properties, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.209-221, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268964]
• 19: Trevor Jim, What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-53, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237728]
• 20: A. J. Kfoury , J. B. Wells, Principality and decidable type inference for finite-rank intersection types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-174, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292556]
• 21: A. J. Kfoury, J. B. Wells. Principality and type inference for intersection types using expansion variables. Supersedes {20}, 2003.
• 22: A. J. Kfoury , J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, v.311 n.1-3, p.1-70, 23 January 2004 [doi>10.1016/j.tcs.2003.10.032]
• 23: Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567077]
• 24: E. K. G. Lopez-Escobar. Proof-functional connectives. In C. Di Prisco, ed., Methods of Mathematical Logic, Proceedings of the 6th Latin-American Symposium on Mathematical Logic, Caracas 1983, vol. 1130 of Lecture Notes in Mathematics. Springer-Verlag, 1985.
• 25: Harry G. Mairson, Deciding ML typability is complete for deterministic exponential time, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.382-401, December 1989, San Francisco, California, United States [doi>10.1145/96709.96748]
• 26: Harry G. Mairson, From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple, Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, p.2-17, December 12-14, 2002
• 27: R. Milner. A theory of type polymorphism in programming. J. Comput. System Sci., 17, 1978.
• 28: Peter Møller Neergaard , Harry G. Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 29: G. Pottinger. A type assignment for the strongly normalizable λ-terms. In Hindley and Seldin {17}.
• 30: L. Regnier. Lambda calcul et réseaux. PhD thesis, University Paris 7, 1992.
• 31: S. Ronchi Della Rocca, Principal type scheme and unification for intersection type discipline, Theoretical Computer Science, v.59 n.1-2, p.181-209, July 1988 [doi>10.1016/0304-3975(88)90101-6]
• 32: S. Ronchi Della Rocca, B. Venneri. Principal type schemes for an extended type theory. Theoret. Comput. Sci., 28(1--2), 1984.
• 33: É. Sayag, M. Mauny. A new presentation of the intersection type discipline through principal typings of normal forms. Technical Report RR-2998, INRIA, 1996.
• 34: Paweł Urzyczyn, Type reconstruction in F _ω, Mathematical Structures in Computer Science, v.7 n.4, p.329-358, August 1997 [doi>10.1017/S0960129597002302]
• 35: S. J. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Catholic University of Nijmegen, 1993.
• 36: Steffen van Bakel, Intersection type assignment systems, Theoretical Computer Science, v.151 n.2, p.385-435, Nov. 27, 1995
• 37: J. B. Wells, The Essence of Principal Typings, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, p.913-925, July 08-13, 2002
• 38: Joe B. Wells , Christian Haack, Branching Types, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.115-132, April 08-12, 2002
• 39: Joe B. Wells , Christian Haack, Branching Types, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.115-132, April 08-12, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Theory

Keywords:
expansion variables, intersection types, lambda-calculus, type inference