Type inference with polymorphic recursion

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Type inference with polymorphic recursion

Full text

Pdf (2.25 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 15 , Issue 2 (April 1993) table of contents

Pages: 253 - 289

Year of Publication: 1993

ISSN:0164-0925

Author

Fritz Henglein

University of Copenhagen

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 86, Citation Count: 45

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/169701.169692 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
	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.
	3	BEN-YELLES, C. Type-assignment in the Lambda-calculus. Ph.D. dissertation, University College, Swansea, UK, 1979.
	4	H.-J. Boehm, Type inference in the presence of type abstraction, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.192-206, June 19-23, 1989, Portland, Oregon, United States
	5	R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
	6	Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
	7	Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
	8	CHOU, C. Relaxation processes: Theory, case studies and applications. Master's thesis, UCLA, Feb. 1986. Tech. Rep. CSD-860057.
	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.
	10	CURRY, H. Modified basic functionality in combinatory logic. Dialectica 23 (1969), 83-92.
	11	CURRY, H., AND FEYS, R. Combinatory Logtc. Vol. I, North-Holland, Amsterdam, 1958.
	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.
	13	DAMAS, L. Type assignment in programming languages. Ph.D. dissertation, Univ. of Edinburgh, 1984.
	14	Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
	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.
	16	Cynthia Dwork , Paris C. Kanellakis , John C. Mitchell, On the sequential nature of unification, Journal of Logic Programming, v.1 n.1, p.35-50, June 1984 [doi>10.1016/0743-1066(84)90022-0]
	17	Elmar Eder, Properties of substitutions and unifications, Journal of Symbolic Computation, v.1 n.1, p.31-46, March 1985 [doi>10.1016/S0747-7171(85)80027-4]
	18	Leo Geurts , Lambert Meertens , Steven Pemberton, ABC programmer's handbook, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	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.
	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.
	21	Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
	22	Fritz Henglein, Fast left-linear semi-unification, Proceedings of the international conference on Advances in computing and information, p.82-91, February 1991, Niagara Falls, Canada
	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.
	24	Fritz Henglein, Type inference and semi-unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.184-197, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62701]
	25	Fritz Henglein , Harry G. Mairson, The complexity of type inference for higher-order lambda calculi, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-130, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99602]
	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.
	27	HINDLEY, R. The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146 (Dec. 1969), 29-60.
	28	J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
	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.
	30	HUDAK, P., AND WADLER, P., EDS. Report on the Programming Language Haskell. Yale Univ., April 1990.
	31	Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
	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.
	33	Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512649]
	34	P. C. Kanellakis , J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-115, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75286]
	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.
	36	Deepak Kapur , David Musser , Paliath Narendran , Jonathan Stillman, Semi-unification, Theoretical Computer Science, v.81 n.2, p.169-187, April 30 1991 [doi>10.1016/0304-3975(91)90189-9]
	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.
	38	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, A proper extension of ML with an effective type-assignment, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-69, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73565]
	39	A. Kfoury , J. Tiuryn , P. Urzyczyn, Computational consequences and partial solutions of a generalized unification problem, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.98-105, June 1989, Pacific Grove, California, United States
	40	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, ML typability is Dexptime-complete, Proceedings of the fifteenth colloquium on CAAP'90, p.206-220, May 1990, Copenhagen, Denmark
	41	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.468-476, May 13-17, 1990, Baltimore, Maryland, United States [doi>10.1145/100216.100279]
	42	J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
	43	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]
	44	Hans Leiß, On Type Inference for Object-Oriented Programming Languages, Proceedings of the 1st Workshop on Computer Science Logic, p.151-172, October 12-16, 1987
	45	LEIB, H. Decidability of semi-unification in two variables. Tech. Rep. INF-2-ASE-9-89, Siemens, Munich, Germany, July 1989.
	46	LEIB, H. Semi-unification and type mference for polymorphic recursion. Tech Rep. INF2- ASE-5-89~ Siemens, Munich, Germany, 1989.
	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.
	48	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]
	49	Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
	50	Lambert Meertens, Incremental polymorphic type checking in B, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.265-275, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567092]
	51	MIniER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sct. 17 (1978), 348-375.
	52	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	53	John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
	54	John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	55	J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
	56	MoRR~S, J. Lambda-Calculus Models ofProgramming Languages. Ph.D. dissertation, MIT, 1968.
	57	Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
	58	Alan Mycroft , Richard A. O'Keefe, A polymorphic type system for PROLOG., Artificial Intelligence, v.23 n.3, p.295-307, August 1984 [doi>10.1016/0004-3702(84)90017-1]
	59	PATERSON, M., AND WEGMAN, W. Linear unification. J. Comput. Syst. Sci. 16 (1978), 158-167.
	60	PUDL~K, P. On a unification problem related to Kreisel's conjecture. Commentationes Math. Univer. Carohnae 29, 3 (1988), 551 556.
	61	P. Purdom, Detecting looping simplifications, on Rewriting techniques and applications, p.54-61, May 1987, Bordeaux, France
	62	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	63	J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
	64	STERHNG, L., AND SHAPmO, E. The Art of PROLOG. MIT Press, 1986.
	65	D Turner, An overview of Miranda, ACM SIGPLAN Notices, v.21 n.12, p.158-166, Dec. 1986 [doi>10.1145/15042.15053]
	66	Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]

CITED BY 45

	Naoki Kobayashi, Type-based useless variable elimination, ACM SIGPLAN Notices, v.34 n.11, p.84-93, Nov. 1999
	Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, ACM SIGPLAN Notices, v.32 n.5, p.261-272, May 1997
	Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States
	H. Seidl , M. H. Sørensen, Constraints to stop higher-order deforestation, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.400-413, January 15-17, 1997, Paris, France
	Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States
	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
	Pascal Fradet, Collecting more garbage, ACM SIGPLAN Lisp Pointers, v.VII n.3, p.24-33, July-Sept. 1994
	François Pessaux , Xavier Leroy, Type-based analysis of uncaught exceptions, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.276-290, January 20-22, 1999, San Antonio, Texas, United States
	Chris Okasaki, Catenable double-ended queues, ACM SIGPLAN Notices, v.32 n.8, p.66-74, Aug. 1997
	Mads Tofte , Lars Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.724-767, July 1998
	Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States
	Mikael Rittri, Dimension inference under polymorphic recursion, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.147-159, June 26-28, 1995, La Jolla, California, United States
	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
	Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, ACM SIGPLAN Notices, v.35 n.5, p.253-263, May 2000
	Chris Okasaki, From fast exponentiation to square matrices: an adventure in types, ACM SIGPLAN Notices, v.34 n.9, p.28-35, Sept. 1999
	Xavier Leroy , François Pessaux, Type-based analysis of uncaught exceptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.340-377, March 2000
	Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Naoki Kobayashi, Type-Based Useless-Variable Elimination, Higher-Order and Symbolic Computation, v.14 n.2-3, p.221-260, September 2001
	C. Barry Jay, The pattern calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.6, p.911-937, November 2004
	Carlos Camarão , Lucília Figueiredo , Cristiano Vasconcellos, Constraint-set satisfiability for overloading, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.67-77, August 24-26, 2004, Verona, Italy
	Wei-Ngan Chin , Siau-Cheng Khoo, Calculating Sized Types, Higher-Order and Symbolic Computation, v.14 n.2-3, p.261-300, September 2001
	Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, ACM SIGPLAN Notices, v.37 n.11, November 2002
	François Pottier , Yann Régis-Gianas, Stratified type inference for generalized algebraic data types, ACM SIGPLAN Notices, v.41 n.1, p.232-244, January 2006
	Peter J. Stuckey , Martin Sulzmann, A theory of overloading, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1216-1269, November 2005
	James Rose , Nikhil Swamy , Michael Hicks, Dynamic inference of polymorphic lock types, Science of Computer Programming, v.58 n.3, p.366-383, December 2005
	Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006
	Andreas Abel , Ralph Matthes , Tarmo Uustalu, Iteration and coiteration schemes for higher-order and nested datatypes, Theoretical Computer Science, v.333 n.1-2, p.3-66, 1 March 2005
	Tom Schrijvers , Maurice Bruynooghe, Polymorphic algebraic data type reconstruction, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, ACM SIGPLAN Notices, v.41 n.6, June 2006
	David L. Heine , Monica S. Lam, Static detection of leaks in polymorphic containers, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
	Vincent Simonet , François Pottier, A constraint-based approach to guarded algebraic data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.1-es, January 2007
	Martin Sulzmann , Meng Wang, Aspect-oriented programming with type classes, Proceedings of the 6th workshop on Foundations of aspect-oriented languages, p.65-74, March 13-13, 2007, Vancouver, British Columbia, Canada
	Michael Furr , Jeffrey S. Foster, Checking type safety of foreign function calls, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-63, July 2008
	Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, ACM SIGPLAN Notices, v.36 n.3, p.54-66, March 2001
	Torben Amtoft , Flemming Nielson , Hanne Riis Nielson, Type and behaviour reconstruction for higher-order concurrent programs, Journal of Functional Programming, v.7 n.3, p.321-347, May 1997
	Ralf Hinze, Generalizing generalized tries, Journal of Functional Programming, v.10 n.4, p.327-351, July 2000
	Ralf Hinze, Perfect trees and bit-reversal permutations, Journal of Functional Programming, v.10 n.3, p.305-317, May 2000
	Satish Chandra , Vijay Saraswat , Vivek Sarkar , Rastislav Bodik, Type inference for locality analysis of distributed data structures, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, February 20-23, 2008, Salt Lake City, UT, USA
	Derek Dreyer, A type system for recursive modules, ACM SIGPLAN Notices, v.42 n.9, September 2007
	Martin Sulzmann , Peter j. Stuckey, Hm(x) type inference is clp(x) solving, Journal of Functional Programming, v.18 n.2, p.251-283, March 2008
	Ferruccio Damiani, Rank 2 Intersection for Recursive Definitions, Fundamenta Informaticae, v.77 n.4, p.451-488, December 2007
	Michael Lienhardt , Alan Schmitt , Jean-Bernard Stefani, Typing communicating component assemblages, Proceedings of the 7th international conference on Generative programming and component engineering, October 19-23, 2008, Nashville, TN, USA
	Didier Rémy , Boris Yakobowski, From ML to ML^F: graphic type constraints with efficient type inference, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Ming Kawaguchi , Patrick Rondon , Ranjit Jhala, Type-based data structure verification, ACM SIGPLAN Notices, v.44 n.6, June 2009