Article

The Essence of Principal Typings

Author:

J. B. WellsAuthors Info & Claims

ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming

Pages 913 - 925

Published: 08 July 2002 Publication History

Abstract

Let S be some type system. A typing in S for a typable term M is the collection of all of the information other than M which appears in the final judgement of a proof derivation showing that M is typable. For example, suppose there is a derivation in S ending with the judgement A M : meaning that M has result type when assuming the types of free variables are given by A . Then ( A , ) is a typing for M . A principal typing in S for a term M is a typing for M which somehow represents all other possible typings in S for M . It is important not to confuse this with a weaker notion in connection with the Hindley/Milner type system often called"principal types". Previous definitions of principal typings for specific type systems have involvedv arious syntactic operations on typings such as substitution of types for type variables, expansion, lifting, etc.This paper presents a new general definition of principal typings which does not depend on the details of any particular type system. This paper shows that the new general definition correctly generalizes previous system-dependent definitions. This paper explains why the new definition is the right one. Furthermore, the new definition is used to prove that certain polymorphic type systems using -quantifiers, namely System F and the Hindley/Milner system, do not have principal typings.All proofs can be foundin a longer version available at the author's home page.

References

[1]

A. Banerjee. A modular, polyvariant, andt ype-basedclosure analysis. In Proc. 1997 Int'l Conf. Functional Programming . ACM Press, 1997.

[2]

M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Principal type schemes and ¿-calculus semantics. In Hindley and Seldin {10}.

[3]

M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Functional characters of solvable terms. Z. Math. LogikGrund lag. Math. , 27(1), 1981.

[4]

M. Coppo, P. Giannini. A complete type inference algorithm for simple intersection types. In 17th Colloq. Trees in Algebra and Programming , vol. 581 of LNCS . Springer-Verlag, 1992.

[5]

H. B. Curry, R. Feys. Combinatory Logic I . Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1958.

[6]

L. Damas, R. Milner. Principal type schemes for functional programs. In Conf. Rec. 9th Ann. ACM Symp. Princ. of Prog. Langs. , 1982.

[7]

J.-Y. Girard. Interprétation Fonctionnelle et Elimination des Coupures de l'Arithmétique d'Ordre Supérieur . Thèse d'Etat, Université de Paris VII, 1972.

[8]

R. Harper, J. C. Mitchell. On the type structure of Standard ML. ACM Trans. on Prog. Langs. & Systs. , 15(2), 1993.

[9]

J. R. Hindley. Basic Simple Type Theory, vol. 42 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press, 1997.

[10]

J. R. Hindley, J. P. Seldin, eds. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism . Academic Press, 1980.

[11]

B. Jacobs, I. Margaria, M. Zacchi. Filter models with polymorphic types. Theoret. Comput. Sci. , 95, 1992.

[12]

T. Jensen. Inference of polymorphic andcond itional strictness properties. In POPL '98 {23}.

[13]

T. Jim. What are principal typings andwhat are they goodfor? Tech. memo. MIT/LCS/TM-532, MIT, 1995.

[14]

T. Jim. What are principal typings andwhat are they goodfor? In Conf. Rec. POPL '96: 23rd ACM Symp. Princ. of Prog. Langs. , 1996.

[15]

A. J. Kfoury, H. G. Mairson, F. A. Turbak, J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int'l Conf. Functional Programming . ACM Press, 1999.

[16]

A. J. Kfoury, J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order ¿-calculus. In Proc. 1994 ACM Conf. LISP Funct. Program. , 1994.

[17]

A. J. Kfoury, 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. , 1999.

[18]

D. Leivant. Polymorphic type inference. In Conf. Rec. 10th Ann. ACM Symp. Princ. of Prog. Langs. , 1983.

[19]

R. Milner. A theory of type polymorphism in programming. J. Comput. System Sci. , 17, 1978.

[20]

R. Milner, M. Tofte, R. Harper, D. B. MacQueen. The Definition of Standard ML (Revised) . MIT Press, 1997.

[21]

J. H. Morris. Lambda-calculus Models of Programming Languages . PhD thesis, Massachusetts Institute of Technology, Cambridge, Mass., U.S.A., 1968.

[22]

B. Pierce. Bounded quantification is undecidable. Inform. & Comput. , 112, 1994.

[23]

Conf. Rec. POPL '98: 25th ACM Symp. Princ. of Prog. Langs. , 1998.

[24]

G. Pottinger. A type assignment for the strongly normalizable ¿-terms. In Hindley and Seld in {10}.

[25]

J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation , vol. 19 of LNCS , Paris, France, 1974. Springer-Verlag.

[26]

S. Ronchi Della Rocca. Principal type schemes and unification for intersection type discipline. Theoret. Comput. Sci. , 59(1-2), 1988.

[27]

S. Ronchi Della Rocca, B. Venneri. Principal type schemes for an extended type theory. Theoret. Comput. Sci. , 28(1-2), 1984.

[28]

A. Schubert. Second-order unification and type inference for Church-style polymorphism. In POPL '98 {23}.

[29]

P. Urzyczyn. Type reconstruction in F _¿. Math. Structures Comput. Sci., 7(4), 1997.

[30]

S. J. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems . PhD thesis, Catholic University of Nijmegen, 1993.

[31]

S. J. van Bakel. Intersection type assignment systems. Theoret. Comput. Sci. , 151(2), 1995.

[32]

J. B. Wells. Typability and type checking in the second-order ¿-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Symp. Logic in Comput. Sci. , 1994. Superseded by {34}.

[33]

J. B. Wells. Typability is undecidable for F+eta. Tech. Rep. 96-022, Comp. Sci. Dept., Boston Univ., 1996.

[34]

J. B. Wells. Typability and type checking in System F are equivalent andund ecidable. Ann. Pure Appl. Logic , 98(1-3), 1999. Supersedes {32}.

Cited By

Szabó TKuci EBijman MMezini MErdweg SDolby JHalfond WMishra A(2018)Incremental overload resolution in object-oriented programming languagesCompanion Proceedings for the ISSTA/ECOOP 2018 Workshops10.1145/3236454.3236485(27-33)Online publication date: 16-Jul-2018
https://dl.acm.org/doi/10.1145/3236454.3236485
Bucciarelli AKesner DVentura D(2016)Strong Normalization through Intersection Types and MemoryElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.06.006323:C(75-91)Online publication date: 11-Jul-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.06.006
Erdweg SBračevac OKuci EKrebs MMezini M(2015)A co-contextual formulation of type rules and its application to incremental type checkingACM SIGPLAN Notices10.1145/2858965.281427750:10(880-897)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814277
Show More Cited By

Index Terms

The Essence of Principal Typings
1. Mathematics of computing
  1. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Logic

Recommendations

What are principal typings and what are they good for?
POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming

July 2002

1065 pages

ISBN:3540438645

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 July 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Szabó TKuci EBijman MMezini MErdweg SDolby JHalfond WMishra A(2018)Incremental overload resolution in object-oriented programming languagesCompanion Proceedings for the ISSTA/ECOOP 2018 Workshops10.1145/3236454.3236485(27-33)Online publication date: 16-Jul-2018
https://dl.acm.org/doi/10.1145/3236454.3236485
Bucciarelli AKesner DVentura D(2016)Strong Normalization through Intersection Types and MemoryElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.06.006323:C(75-91)Online publication date: 11-Jul-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.06.006
Erdweg SBračevac OKuci EKrebs MMezini M(2015)A co-contextual formulation of type rules and its application to incremental type checkingACM SIGPLAN Notices10.1145/2858965.281427750:10(880-897)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814277
Erdweg SBračevac OKuci EKrebs MMezini MAldrich JEugster P(2015)A co-contextual formulation of type rules and its application to incremental type checkingProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2814270.2814277(880-897)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2814270.2814277
Simon A(2014)Optimal inference of fields in row-polymorphic recordsACM SIGPLAN Notices10.1145/2666356.259431349:6(100-111)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2666356.2594313
Simon AO'Boyle MPingali K(2014)Optimal inference of fields in row-polymorphic recordsProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2594291.2594313(100-111)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2594291.2594313
Simon A(2014)Deriving a complete type inference for Hindley-Milner and vector sizes using expansionScience of Computer Programming10.1016/j.scico.2014.03.00595:P2(254-271)Online publication date: 1-Dec-2014
https://dl.acm.org/doi/10.1016/j.scico.2014.03.005
Simon AAlbert EMu S(2013)Deriving a complete type inference for hindley-milner and vector sizes using expansionProceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation10.1145/2426890.2426895(13-22)Online publication date: 21-Jan-2013
https://dl.acm.org/doi/10.1145/2426890.2426895
Lenglet SWells J(2012)Expansion for universal quantifiersProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_23(456-475)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_23
Hunt SSands D(2011)From exponential to polynomial-time security typing via principal typesProceedings of the 20th European conference on Programming languages and systems: part of the joint European conferences on theory and practice of software10.5555/1987211.1987227(297-316)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987211.1987227
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents