Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)

Abstract

We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ₁ Λ τ₂ to be used in some places at type τ₁ and in other places at type τ₂. A finite-rank intersection type system bounds how deeply the Λ can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorphism of System F and its extensions, while typing many more programs than the Hindley-Milner type system found in ML and Haskell.While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let K(0, n) = n and K(t + 1, n) = 2^K(t,n); we prove that recognizing the pure λ-terms of size n that are typable at rank k is complete for DTIME[K(k−1, n)]. We then consider the problem of deciding whether two λ-terms typable at rank k have the same normal form, generalizing a well-known result of Statman from simple types to finite-rank intersection types. We show that the equivalence problem is DTIME[K(K(k − 1, n), 2)]-complete. This relationship between the complexity of typability and expressiveness is identical in wellknown decidable type systems such as simple types and Hindley-Milner types, but seems to fail for System F and its generalizations. The correspondence gives rise to a conjecture that if Τ is a predicative type system where typability has complexity t(n) and expressiveness has complexity e(n), then t(n) = Ω(log* e(n)).

References

1. AM98 A. Asperti and H. G. Mairson. Parallel beta reduction is not elementary recursive. In Conference Record of POPL '98: The ~5th AGM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 303-315, San Diego, California, 19-21 Jan. 1998.
2. vB93 S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Catholic University of Nijmegen, 1993.
3. Bar84 H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.
4. CDCV80 M. Coppo, M. Dezani-Ciancaglinl, and B. Venneri. Principal type schemes and ,k-calculus semantics. In J. P. Seldin and J. R. Hindley, eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 535-560. Academic Press, 1980.
5. CDCV81 M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift fiir Mathematishche Logik und Grundlagen der Mathematik, 27:45-58, 1981.
6. HM94 F. Henglein and H. G. Mairson. The complexity of type inference for higher-order typed lambda calculi. J. Funct. Prey., 4(4):435-478, Oct. 1994.
7. Jim96 T. Jim. What are principal typings and what are they good for? In Conf. Rec. POPL '96: 23rd A CM Syrup. Principles of Prog. Languages, 1996.
8. Kam96 F. Kamareddine. A reduction relation for which postponement of k-contractions, conservation and preservation of strong normalisation hold. Technical Report TR- 1996-11, Univ. of Glasgow, Glasgow G12 8QQ, Scot- !and, Mar. 1996.
9. KHM94 P. C. Kanellakis, G. G. Hillebrand, and H. G. Muirson. An analysis of the Core-ML language: Expressive power and type reconstruction. In 21st int'l Colloq. on Automata, Languages, and Programming, vol. 820 of LNCS, pp. 83-106, 1994. Invited paper.
10. KRW98 F. Kamareddine, A. Rios, and J. B. Wells. Calculi of generalised/~-reduction and explicit substitutions: The type free and simply typed versions. J. Functional ~4 Logic Programming, 1998(5), June 1998.
11. KT92 A. J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments of the second-order A-calculus. Inf. ~ Comput., 98(2):228-257, June 1992.
12. KW94 A. J. Kfoury and J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the secondorder )~-calculus. In Prec. 199,$ A CM Conf. LISP Funct. Program., 1994.
13. KW95 A. J. Kfoury and J. B. Wells. Addendum to "New notions of reduction and non-semantic proofs of/3-strong normalization in typed A-calculi". Tech. Rep. 95-007, Comp. Sci. Dept., Boston Univ., 1995.
14. KW99 A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Conf. Rec. POPL '99: 26th ACM Syrup. Principles of Prog. Languages, 1999.
15. Lei83 D. Leivant. Polymorphic type inference, in Conf. Rec. lOth Ann. A CM Syrup. Principles of Programming Languages, pp. 88-98, 1983.
16. Mai90 H. G. Mairson. Deciding ML typability is complete for deterministic exponential time. In Conf. Rec. 17th Ann. A CM Syrup. Principles of Programming Languages, pp. 382-401, 1990.
17. Mai92 H. G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2);387-394, Sept. 1992.
18. Mey74 A. R. Meyer. The inherent computational complexity of theories of ordered sets. In Proceedings of the International Congress of Mathematicians., pp. 477-482, 1974.
19. Mit96 J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
20. RDRV84 S. Ronchi Della Rocca and B. Venneri. Principal type schemes for an extended type theory. Theor. Comp. Sc., 28:151-169, 1984.
21. Sch81 H. Schwichtenberg. Complexity of normalization in the pure typed lambda-calculus. In A. S. Troelstra and D. van Dalen, eds., Proceedings L. E. J. Brouwer Centenary Syrup., vet. 110 of Studies in Logic and the Foundations of Mathematics, pp. 453-457, Noordwijkerhout, The Netherlands, June8-13, 1981. North- Holland, Amsterdam. Published in 1982.
22. Sta79 Ft. Statman. The typed lambda -calculus is not elementary recursive. Theoretical Computer Science, 9(1):73- 81, July 1979.
23. WDMT97 J. B. Wells, A. Dimock, R. Muller, and F. Turbak. A typed intermediate language for flow-directed compilation. In Prec. 7th {nt'l Joint Conf. Theory ~4 Practice of Software Development, 1997. Superseded by {WDMT9X}.
24. WDMT9X J. B. Wells, A. Dimock, R. Muller, and F. Turbak. A calculus with polymorphlc and polyvariant flow types. J. Funct. Prog., 199X. To appear after revisions. Supersedes {WDMT97}.

Index Terms

• Theory of computation

  • Semantics and reasoning

    • Program semantics