article

Open access

Type inference with polymorphic recursion

Editor: Andrew W. Appel Author:

Fritz HengleinAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 15, Issue 2

Pages 253 - 289

https://doi.org/10.1145/169701.169692

Published: 01 April 1993 Publication History

PDF eReader

References

[1]

AHO, A., SETHI, R., AND ULLMAN, J. Comp~lers: Princ~ples, Technzques, and Tools. Addlson- Wesley, Reading, Mass., 1986. Addison-Wes}ey, 1986, Reprinted w~th corrections, March 1988.

Crossref

Google Scholar

[2]

BARENDREGT, H. The Lambda calculus: Its syntax and semantics. In Studies in Logzc and the Foundations of Mathematics, vol 103. North-Holland, Amsterdam, 1984.

Google Scholar

[3]

BEN-YELLES, C. Type-assignment in the Lambda-calculus. Ph.D. dissertation, University College, Swansea, UK, 1979.

Google Scholar

[4]

BOEHM, H. Type inference in the presence of type abstraction. In Proceedmgs of the SIGPLAN '89 Conference on Programm~ng Language Design and hnplementatlon (June 1989), ACM, ACM Press, New York, 1989, 192-206.

Crossref

Google Scholar

[5]

BURSTALL, R., MACQUEEN, D., AND SANNELLA, D. Hope: An experimental applicative language. In Stanford LISP Conference 1980 (1980), 136-143.

Crossref

Google Scholar

[6]

CARDELLI, L. A semantics of multiple inheritance. Inf. Comput. (Inf. Control), 76 (1988), 138-164.

Crossref

Google Scholar

[7]

CARDELLI, L., AND WEGNER, P. On understanding types, data abstraction and polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471-522.

Crossref

Google Scholar

[8]

CHOU, C. Relaxation processes: Theory, case studies and applications. Master's thesis, UCLA, Feb. 1986. Tech. Rep. CSD-860057.

Google Scholar

[9]

CLEMENT, D., DESPEYROUX, J., DESPEYROUX, T., AND KAHN, G. A simple applicative language: Mini-ML. INRIA Centre, Sophia Antipolis, RR No. 529, May 1986.

Google Scholar

[10]

CURRY, H. Modified basic functionality in combinatory logic. Dialectica 23 (1969), 83-92.

Google Scholar

[11]

CURRY, H., AND FEYS, R. Combinatory Logtc. Vol. I, North-Holland, Amsterdam, 1958.

Google Scholar

[12]

CURRY, H., HINDLEY, J., AND SELDIN, J. C"mblnatory Logic. Vol. II, Studies in Logie and the Foundations of Mathematics, North-Holland, Amsterdam, 1972.

Google Scholar

[13]

DAMAS, L. Type assignment in programming languages. Ph.D. dissertation, Univ. of Edinburgh, 1984.

Google Scholar

[14]

DAMAS, L., AND MILNER, R. Principal type schemes for functional programs. In Proceedings of the 9th Annual ACM Symposzum on Princtples of Programming Languages (Jan. 1982), 207-212.

Crossref

Google Scholar

[15]

D"RRE, J., AND ROUNDS, W. On subsumption and semiunification in feature algebras. In Proceedings of the 1990 IEEE Symposium on Logtc in Computer Science (LICS). IEEE Computer Society Press, 1990, 300-311.

Google Scholar

[16]

DWORK, C., KANELLAKIS, P., AND MITCHELL, J. On the sequential nature of unifcation. J. Logic Program. I (1984), 35-50.

Crossref

Google Scholar

[17]

EDER, E. Properties of substitutions and unifications. J. Symb. Comput. I (1985), 31-46.

Crossref

Google Scholar

[18]

GEURTS, L., MEERTENS, L., AND PEMBERTON, S. The ABC Programmer's Handbook. Prentice- Hall, New York, 1990.

Crossref

Google Scholar

[19]

GIANNINI, P., AND RONCHI DELLA ROCCA, S. Characterization of typings in polymorphic type discipline. In Proceedings of the Symposium on Logic in Computer Science (1988). IEEE Computer Society Press, 1988, 61-70.

Google Scholar

[20]

GmARD, J. Une extension de l'interpretation de Godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In 2nd Scandinavian Logic Symposium (1971), 63-92. In French.

Google Scholar

[21]

GIRARD, J., LAFONT, Y., AND TAYLOR, P. Proofs and Types. Vol. 7, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

Crossref

Google Scholar

[22]

HENGLEIN, F. Fast left-linear semiunification. In Proceedings of the Internattonal Conference on Computing and Information. Lecture Notes of Computer Science, vol. 468, Springer- Verlag, New York, 1990.

Crossref

Google Scholar

[23]

HEN6LEIN, F. Polymorphic type inference and semi-unification. Ph.D. dissertation, Rutgers Univ., April 1989. Available as NYU Tech. Rep. 443, May 1989, from New York University, Courant Institute of Mathematical Sciences, Department of Computer Science.

Google Scholar

[24]

HENGLEtN, F. Type inference and semi-unification. In Proceedtngs of the ACM Conference on LISP and Functional Programming (LFP) (Snowbird, Utah, July 1988), ACM Press, New York, 1988, 184-197.

Crossref

Google Scholar

[25]

HENGLEIN, F., AND MAIRSON, H. The complexity of type inference for higher-order typed lambda calculi. In Proceedtngs of the 18th ACM Symposium on Principles of Programming Languages (POPL) (Orlando, Fl., Jan. 1991), ACM Press, New York, 1991, 119-130.

Crossref

Google Scholar

[26]

HERBRAND, J. Recherches sur la theorie de la demonstration. In Ecrits logtques de Jacques Herbrand, PUF, Paris, 1968. Th~se de Doctorat d'Etat, Universit~ de Paris, 1930. In French.

Google Scholar

[27]

HINDLEY, R. The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146 (Dec. 1969), 29-60.

Google Scholar

[28]

HtNDLEY, R., AND SELmN, J. Introduction to Combinators and A-Calculus. Vol. 1, London Mathematical Society Student Texts, Cambridge University Press, 1986.

Crossref

Google Scholar

[29]

HOOPER, P. The undeeidability of the Turing machine immortality problem. Ph.D. dissertation, Harvard Univ., June 1965. Computation Lab. Rep. BL-38; also in J. Symbolic Logic, 1966.

Google Scholar

[30]

HUDAK, P., AND WADLER, P., EDS. Report on the Programming Language Haskell. Yale Univ., April 1990.

Google Scholar

[31]

HUET, G Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27, 4 (Oct. 1980), 797-821.

Crossref

Google Scholar

[32]

HUET, G. R~solution d'equations dans des langages d'ordre 1, 2,., omega (Th~se de Doctorat d'Etat). Univ. Paris VII, Sept. 1976.

Google Scholar

[33]

JOHNSON, G., AND WALZ, J. A max~mum-fiow approach to anomaly isolation in unificationbased incremental type inference. In Proceedmgs of the 13th Annua! ACM Symposzum on Principles ofProgrammtng Languages (Jan. 1986), ACM, New York, 1986, 44 57.

Crossref

Google Scholar

[34]

KANELLAKIS, P., AND MITCHELL, J. Polymorphic unification and ML typing (extended abstract). In Proceedzngs of the 16th Annual ACM OEympos~um on Prtnctples of Programmmg Languages (Jan 1989), ACM, New York, 1989.

Crossref

Google Scholar

[35]

KANELLAKIS, P, MAIRSON, H., AND MITCHELL, J. Unification and ML type reconstruction. In Computatlonal Logtc Essays zn Honor of Alan Robmson, J.-L. Lassez and G. Plotkin. Eds. MIT Press, 1991.

Google Scholar

[36]

KAPUR, D., MUSSER, D., NARENDRAN, P, AND STILLMAN, J. Semi-unification. Tbeor. Comput. Set. 81, 2 (Apr. 1991), 169 188. Based on paper presented at Conference on Foundations of Software Technology and Theoretzcal Computer Sctence (FST-TCS), Dec. 1988.

Crossref

Google Scholar

[37]

KFOURY, A, AND TWR~, J. Type reconstruction in finite-rank fragments of the polymorphlc A-calculus. In Proceedings of the 5th Annual IEEE OEymposzum on Logzc in Computer Science (LICS) (Phfiadelphla, June 1990), IEEE Computer Society Press, New York, 1990, 2 11.

Google Scholar

[38]

KFOURY, A., TIURYN, J., AND URZYCZYN, P. A proper extension of ML with an effective type-assignment. In Proceedtngs of the 15th Annual ACM Symposium on Princtples of Programmmg Languages (Jan. 1988), ACM Press, New York, 58 69.

Crossref

Google Scholar

[39]

KrouRv, A., TIURYN, J., AND URZ~CZYN, P. Computational consequences and partial solutions of a generahzed unification problem. In Proceedmgs of the 4th IEEE Symposium on Loglc in Computer Science (LICS) (June 1989).

Crossref

Google Scholar

[40]

KFOURY, A., TmRYN, J., AND URZ~CZYN, P. ML typabihty ~s DEXPTIME-complete. In Proceedtngs of the 15th Colloqzum on Trees in Algebra and Programming (CAAP) (Copenhagen, May 1990), Lecture Notes in Computer Science, vol. 431, Springer, New York, 1990, 206 220.

Crossref

Google Scholar

[41]

KFOURY, A., TmRYN, J., AND URZY~ZYN, P. The undecidability of the semi-umfication problem. In Proceedings of the 22nd Annual ACM OEymposium on T,beorv of Computatzon (STOC) (Baltimore, Md., May 1990), ACM, New York, 1990, 468 476.

Crossref

Google Scholar

[42]

LASSEZ, J., MAHER, M, AND MARRIOTT, K. Unification revisited. In Foundattons of Dedt~tzve Databases and Loglc Programming, J. Minker, Ed., Morgan Kauffman, Palo Alto, Calif., 1987.

Crossref

Google Scholar

[43]

LEtVANT, D. Polymorphic type inference. In Proceedtng~ of the lOth ACM Symposium on Prtnctples ofProgrammzng Languages (Jan. 1983), ACM, New York, 1983, 88-98.

Crossref

Google Scholar

[44]

LEIB, H. On type inference for object-oriented programming languages. In Proceedings of the 1st Workshop on Computer Sctence Loglc (Oct. 1987), Lecture Notes in Computer Science, vol. 329, Springer, New York, 1987.

Crossref

Google Scholar

[45]

LEIB, H. Decidability of semi-unification in two variables. Tech. Rep. INF-2-ASE-9-89, Siemens, Munich, Germany, July 1989.

Google Scholar

[46]

LEIB, H. Semi-unification and type mference for polymorphic recursion. Tech Rep. INF2- ASE-5-89~ Siemens, Munich, Germany, 1989.

Google Scholar

[47]

LEIB, H., AND HENGLEIN, F. A decidable case of the semi-umfication problem. In Proceedtngs of the 16th Internattonal Sympostum on Mathematlcal Foundations of Computer Science (MFCS), (Sept. 1991), Lecture Notes in Computer Science, Springer, New York, 1991.

Google Scholar

[48]

MAIRSON, H. Deciding ML typabihty is complete for deterministic exponential tlme. In Proceedings of the 17th ACM OEymposium on Prmctples of Programmlng Languages ( POPL ) (Jan. 1990), ACM, New York. 1990.

Crossref

Google Scholar

[49]

MARTELLI, A., AND MONTANARI, U. An efficient unification algorithm. ACM Trans. Program. Lang Syst. 4, 2 (Apr. 1982), 258-282.

Crossref

Google Scholar

[50]

MEEgTENS, L. Incremental polymorphic type checking in B In Proceedings ofthe lOth ACM Symposium on Principles of Programmmg Languages (POPL). ACM, New York, 1983, 265-275.

Crossref

Google Scholar

[51]

MIniER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sct. 17 (1978), 348-375.

Google Scholar

[52]

MmNER, R., TOFTE, M., AND HARPER, R. The Definition of Standard ML. MIT Press, 1990.

Crossref

Google Scholar

[53]

M~TCHELL, J. Polymorphic type inference and containment. Inf. Control 76 (1988), 211-249.

Crossref

Google Scholar

[54]

MITCHELL, J. Type systems for programming languages. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed., North-Holland, Amsterdam, 1990.

Crossref

Google Scholar

[55]

MITCHELL, J., AND HARPER, R. The essence of ML. In Proceedtngs of the 15th ACM Symposium on Principles of Programming Languages ( POPL ) (Jan. 1988), ACM, New York, 1988.

Crossref

Google Scholar

[56]

MoRR~S, J. Lambda-Calculus Models ofProgramming Languages. Ph.D. dissertation, MIT, 1968.

Google Scholar

[57]

MYCROFT, A. Polymorphic type schemes and recursive definitions. In Proceedings ofthe 6th International Conference on Programming, LNCS 167 (1984).

Crossref

Google Scholar

[58]

M~CROFT, A., AND O'KEEFE, R. A polymorphic type system for PROLOG. Artif. Intell. 23 (1984), 295-307.

Crossref

Google Scholar

[59]

PATERSON, M., AND WEGMAN, W. Linear unification. J. Comput. Syst. Sci. 16 (1978), 158-167.

Google Scholar

[60]

PUDL~K, P. On a unification problem related to Kreisel's conjecture. Commentationes Math. Univer. Carohnae 29, 3 (1988), 551 556.

Google Scholar

[61]

PURDOM, P. Detecting looping simplifications. In Proceedings of the 2nd Conference on Rewrite Rule Theory and Applications (RTA) (May 1987), Springer, New York, 1987, 54-62.

Crossref

Google Scholar

[62]

REYNOLDS, J. Towards a theory of type structure. In Proceedings of the Programming Symposium. Springer, 1974, 408-425.

Crossref

Google Scholar

[63]

SCHWARTZ, J., DEWAR, R., DUSINSKY, E., AND SCHONBERO, E. Programming with Sets: An Introduction to SETL. Springer, New York, 1986.

Crossref

Google Scholar

[64]

STERHNG, L., AND SHAPmO, E. The Art of PROLOG. MIT Press, 1986.

Google Scholar

[65]

TURNER, D. An overview of Miranda. SIGPLANNot. 21, 12 (Dec. 1986), 158-166.

Crossref

Google Scholar

[66]

W~3qD, M. Finding the source of type errors. In Proceedings of the IEEE Symposium on Logtc in Computer Science (June 1986), IEEE, New York, 1986, 38-43.

Crossref

Google Scholar

Cited By

View all

Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Vasileva ABugayenko Y(2023)Object Specialization to Partially Reduce Polymorphism of AttributesProceedings of the 2023 7th International Conference on Computer Science and Artificial Intelligence10.1145/3638584.3638674(106-115)Online publication date: 8-Dec-2023
https://dl.acm.org/doi/10.1145/3638584.3638674
Colaço JPauget BPouzet MHenriksen TSinkarovs A(2023)Polymorphic Types with Polynomial SizesProceedings of the 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming10.1145/3589246.3595372(36-49)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589246.3595372
Show More Cited By

Index Terms

Type inference with polymorphic recursion

Recommendations

Polymorphic type inference and abstract data types

Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Polymorphism, subtyping, and type inference in MLsub
POPL '17

We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 15, Issue 2

April 1993

155 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/169701

Editor:
Andrew W. Appel
Princeton Univ., Princeton, NJ

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1993

Published in TOPLAS Volume 15, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

143
Total Citations
View Citations
1,666
Total Downloads

Downloads (Last 12 months)156
Downloads (Last 6 weeks)13

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Vasileva ABugayenko Y(2023)Object Specialization to Partially Reduce Polymorphism of AttributesProceedings of the 2023 7th International Conference on Computer Science and Artificial Intelligence10.1145/3638584.3638674(106-115)Online publication date: 8-Dec-2023
https://dl.acm.org/doi/10.1145/3638584.3638674
Colaço JPauget BPouzet MHenriksen TSinkarovs A(2023)Polymorphic Types with Polynomial SizesProceedings of the 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming10.1145/3589246.3595372(36-49)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589246.3595372
Schimpf AWehr SBieniusa A(2022)Set-theoretic Types for ErlangProceedings of the 34th Symposium on Implementation and Application of Functional Languages10.1145/3587216.3587220(1-14)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3587216.3587220
Ângelo PFlorido M(2022)Type Inference for Rank-2 Intersection Types Using Set UnificationTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_29(462-480)Online publication date: 27-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17715-6_29
Hinze RSwierstra W(2022)Calculating DatastructuresMathematics of Program Construction10.1007/978-3-031-16912-0_3(62-101)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16912-0_3
Barbosa JFlorido MCosta V(2021)Data Type Inference for Logic ProgrammingLogic-Based Program Synthesis and Transformation10.1007/978-3-030-98869-2_2(16-37)Online publication date: 7-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-98869-2_2
Fachinetti LPalmer ZSmith SWu KYorihiro A(2020)A Set-Based Context Model for Program AnalysisProgramming Languages and Systems10.1007/978-3-030-64437-6_1(3-24)Online publication date: 30-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64437-6_1
Thorand FHage J(2020)Higher-Ranked Annotation Polymorphic Dependency AnalysisProgramming Languages and Systems10.1007/978-3-030-44914-8_24(656-683)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_24
Barbosa JFlorido MSantos Costa V(2019)A Three-Valued Semantics for Typed Logic ProgrammingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.306.10306(36-51)Online publication date: 19-Sep-2019
https://doi.org/10.4204/EPTCS.306.10
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

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

References

Cited By

Index Terms

Recommendations

Polymorphic type inference and abstract data types

Type checking and inference for polymorphic and existential types

Polymorphism, subtyping, and type inference in MLsub

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations