skip to main content
article

Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

Published: 19 September 2004 Publication History

Abstract

Useful type inference must be faster than normalization. Otherwise, you could check safety conditions by running the program. We analyze the relationship between bounds on normalization and type inference. We show how the success of type inference is fundamentally related to the amnesia of the type system: the nonlinearity by which all instances of a variable are constrained to have the same type.Recent work on intersection types has advocated their usefulness for static analysis and modular compilation. We analyze System-I (and some instances of its descendant, System E), an intersection type system with a type inference algorithm. Because System-I lacks idempotency, each occurrence of a variable requires a distinct type. Consequently, type inference is equivalent to normalization in every single case, and time bounds on type inference and normalization are identical. Similar relationships hold for other intersection type systems without idempotency.The analysis is founded on an investigation of the relationship between linear logic and intersection types. We show a lockstep correspondence between normalization and type inference. The latter shows the promise of intersection types to facilitate static analyses of varied granularity, but also belies an immense challenge: to add amnesia to such analysis without losing all of its benefits.

References

[1]
H. Abelson and G. J. Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1985.
[2]
R. Amadio and P.-L. Curien. Domains and Lambda Calculi, volume 46 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1998.
[3]
A. Asperti and S. Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1998.
[4]
A. Banerjee. A modular, polyvariant, and type-based closure analysis. In Proc. 1997 Int'l Conf. Functional Programming. ACM Press, 1997.
[5]
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.
[6]
S. Carlier, J. Polakow, J. B. Wells, and 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, volume 2986 of LNCS, pages 294--309. Springer-Verlag, 2004.
[7]
S. Carlier and J. B. Wells. Type inference with expansion variables and intersection types in System E and an exact corre-spondence with β -reduction. Technical Report HW-MACS-TR-0012, Heriot-Watt Univ., School of Math. & Comput. Sci., Jan. 2004.
[8]
M. Coppo, F. Damiani, and P. Giannini. Strictness, totality, and non-standard type inference. Theoret. Comput. Sci., 272(1-2):69--111, Feb. 2002.
[9]
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Z. Math. Logik Grundlag. Math., 27(1):45--58, 1981.
[10]
F. Damiani. A conjunctive type system for useless-code elimination. Math. Structures Comput. Sci., 13:157--197, 2003.
[11]
F. Damiani. Rank 2 intersection types for local definitions and conditional expressions. ACM Trans. on Prog. Langs. & Systs., 25(4):401--451, 2003.
[12]
F. Damiani. Rank 2 intersection types for modules. In Proc. 5th Int'l Conf. Principles & Practice Declarative Programming, pages 67--78, 2003.
[13]
F. Damiani and P. Giannini. Automatic useless-code detection and elimination for HOT functional programs. J. Funct. Programming, pages 509--559, 2000.
[14]
V. Danos and L. Regnier. The structure of multiplicatives. Arch. Math. Logic, 26, 1989.
[15]
G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In Conf. Rec. 19th Ann. ACM Symp. Princ. of Prog. Langs., pages 15--26, 1992.
[16]
G. Gonthier, M. Abadi, and J.-J. Lévy. Linear logic without boxes. In Proc. 7th Ann. IEEE Symp. Logic in Comput. Sci., pages 223--34. IEEE Comput. Soc. Press, 1992.
[17]
F. Henglein and H. G. Mairson. The complexity of type inference for higher-order typed lambda calculi. J. Funct. Programming, 4(4):435--478, Oct. 1994.
[18]
J. R. Hindley. The principal type scheme of an object in combinatory logic. Trans. American Mathematical Society, 146:29--60, Dec. 1969.
[19]
J. R. Hindley and J. P. Seldin, editors. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
[20]
T. Jensen. Inference of polymorphic and conditional strictness properties. In Conf. Rec. POPL '98: 25th ACM Symp. Princ. of Prog. Langs., 1998.
[21]
T. Jim. What are principal typings and what are they good for? In Conf. Rec. POPL '96: 23rd ACM Symp. Princ. of Prog. Langs., 1996.
[22]
P. Kanellakis, H. Mairson, and J. C. Mitchell. Unification and ML type reconstruction. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.
[23]
A. J. Kfoury. A linearization of the lambda-calculus. J. Logic Comput., 10(3), 2000.
[24]
A. J. Kfoury, H. G. Mairson, F. A. Turbak, and J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int'l Conf. Functional Programming, pages 90--101. ACM Press, 1999.
[25]
A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. ML typability is DEXPTIME complete. In 15th Colloq. Trees in Algebra and Programming, volume 431 of LNCS, pages 206--220. Springer-Verlag, 1990.
[26]
A. J. Kfoury, G. Washburn, and J. B. Wells. Implementing compositional analysis using intersection types with expansion variables. In Proceedings of the 2nd Workshop on Intersection Types and Related Systems, 2002.
[27]
A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Conf. Rec. POPL '99: 26th ACM Symp. Princ. of Prog. Langs., pages 161--174, 1999.
[28]
A. J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci., 311(1-3):1--70, 2004.
[29]
Y. Lafont. From proof-nets to interaction nets. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, Proceedings of the 1993 Workshop on Linear Logic, London Math. Soc. Lecture Note Series 222, pages 225--247. Cambridge University Press, 1995.
[30]
J. Lamping. An algorithm for optimal lambda-calculus reductions. In POPL '90 {38}, pages 16--30.
[31]
J.-J. Lévy. Optimal reductions in the lambda-calculus. In Hindley and Seldin {19}, pages 159--191.
[32]
H. G. Mairson. Deciding ML typability is complete for deterministic exponential time. In POPL '90 {38}, pages 382--401.
[33]
H. G. Mairson. Outline of a proof theory of parametricity. In FPCA '91, Conf. Funct. Program. Lang. Comput. Arch., volume 523 of LNCS, pages 313-327, Cambridge, MA. U.S.A., 1991. Springer-Verlag.
[34]
H. G. Mairson. From Hilbert spaces to Dilbert spaces: Context semantics made simple. In 22 nd Conference on Foundations of Software Technology and Theoretical Computer Science, 2002.
[35]
R. Milner. A theory of type polymorphism in programming. J. Comput. System Sci., 17:348--375, 1978.
[36]
J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 365--458. North-Holland, 1990.
[37]
C. Mossin. Exact flow analysis. Math. Structures Comput. Sci., 13:125--156, 2003.
[38]
Conf. Rec. 17th Ann. ACM Symp. Princ. of Prog. Langs., 1990.
[39]
L. Regnier. Lambda calcul et réseaux. PhD thesis, University Paris 7, 1992.
[40]
S. Ronchi Della Rocca. Principal type schemes and unification for intersection type discipline. Theoret. Comput. Sci., 59(1-2):181--209, Mar. 1988.
[41]
S. Ronchi Della Rocca and B. Venneri. Principal type schemes for an extended type theory. Theoret. Comput. Sci., 28(1-2):151--169, Jan. 1984.
[42]
É. Sayag and M. Mauny. A new presentation of the intersection type discipline through principal typings of normal forms. Technical Report RR-2998, INRIA, Oct. 16, 1996.
[43]
R. Statman. The typed lambda-calculus is not elementary recursive. Theoret. Comput. Sci., 9(1):73--81, July 1979.
[44]
S. J. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Catholic University of Nijmegen, 1993.
[45]
P. Wadler. Theorems for free! In Proceedings 4th Int. Conf. on Funct. Program. Languages and Computer Architecture, pages 347--359. ACM, 1989.
[46]
G. Washburn, A. Kfoury, J. Wells, B. Alan, B. Yates, O. Schwartz, and S. Carlier. System I experimentation tool. http://types.bu.edu/modular/compositional/experimentation-tool/.
[47]
J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1-3):111--156, 1999.
[48]
J. B. Wells, A. Dimock, R. Muller, and F. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 12(3):183--227, May 2002.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 39, Issue 9
ICFP '04
September 2004
254 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1016848
Issue’s Table of Contents
  • cover image ACM Conferences
    ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming
    September 2004
    264 pages
    ISBN:1581139055
    DOI:10.1145/1016850
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2004
Published in SIGPLAN Volume 39, Issue 9

Check for updates

Author Tags

  1. complexity
  2. idempotence
  3. intersection types
  4. normalization
  5. proofnet
  6. type inference

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)8
  • Downloads (Last 6 weeks)2
Reflects downloads up to 07 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Structural Rules and Algebraic Properties of Intersection TypesTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_6(60-77)Online publication date: 3-Oct-2022
  • (2019)Quantitative Types: From Foundations to ApplicationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.293.1293(1-5)Online publication date: 23-Apr-2019
  • (2018)Types of FireballsProgramming Languages and Systems10.1007/978-3-030-02768-1_3(45-66)Online publication date: 22-Oct-2018
  • (2016)Reasoning About Call-by-need by Means of TypesFoundations of Software Science and Computation Structures10.1007/978-3-662-49630-5_25(424-441)Online publication date: 2016
  • (2015)A Resource Aware Computational Interpretation for Herbelin's SyntaxProceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 939910.1007/978-3-319-25150-9_23(388-403)Online publication date: 29-Oct-2015
  • (2014)The Inhabitation Problem for Non-idempotent Intersection TypesAdvanced Information Systems Engineering10.1007/978-3-662-44602-7_26(341-354)Online publication date: 2014
  • (2014)Quantitative Types for the Linear Substitution CalculusAdvanced Information Systems Engineering10.1007/978-3-662-44602-7_23(296-310)Online publication date: 2014
  • (2024)Extending the Quantitative Pattern-Matching ParadigmProgramming Languages and Systems10.1007/978-981-97-8943-6_5(84-105)Online publication date: 23-Oct-2024
  • (2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
  • (2022)Multi types and reasonable spaceProceedings of the ACM on Programming Languages10.1145/35476506:ICFP(799-825)Online publication date: 31-Aug-2022
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media