Rank 2 intersection types for local definitions and conditional expressions

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Rank 2 intersection types for local definitions and conditional expressions

Full text

Pdf (609 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 25 , Issue 4 (July 2003) table of contents

Pages: 401 - 451

Year of Publication: 2003

ISSN:0164-0925

Author

Ferruccio Damiani

Università di Torino, Torino, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 27, Citation Count: 4

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	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/778559.778560 What is a DOI?

ABSTRACT

We propose a rank 2 intersection type system with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and match-expressions). This is a further step towards the use of intersection types in "real" programming languages.The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 intersection), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to "limit the use" of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might also be useful for other type systems.

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	Shail Aditya , Rishiyur S. Nikhil, Incremental polymorphism, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.379-405, June 1991, Cambridge, Massachusetts, United States
	2	Barendregt, H. P., Coppo, M., and Dezani-Ciancaglini, M. 1983. A filter lambda model and the completeness of type assignment. J. Symb. Logic 48, 931--940.
	3	Mario Coppo, An Extended Polymorphic Type System for Applicative Languages, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.194-204, September 01-05, 1980
	4	Coppo, M. and Dezani-Ciancaglini, M. 1980. An extension of basic functional theory for lambda-calculus. Notre Dame J. Formal Logic 21, 4, 685--693.
	5	Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. 1980. Principal Type Schemes and Lambda-calculus Semantics. In To H. B. Curry. Essays on Combinatory Logic, Lambda-calculus and Formalism, R. Hindley and J. Seldin, Eds. Accademic Press, London, 480--490.
	6	Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. 1981. Functional Characters of Solvable Terms. Zeith. Math. Logik Und Grund. Math. 27, 45--58.
	7	Mario Coppo , Paola Giannini, Principal types and unification for simple intersection type systems, Information and Computation, v.122 n.1, p.70-96, Oct. 1995 [doi>10.1006/inco.1995.1141 ]
	8	Damas, L. M. M. 1984. Type Assignment in Programming Languages. Ph.D. thesis, University of Edinburgh.
	9	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]
	10	Ferruccio Damiani, Typing Local Definitions and Conditional Expressions with Rank 2 Intersection, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, p.82-97, March 25-April 02, 2000
	11	Ferruccio Damiani , Paola Giannini, A Decidable Intersection Type System based on Relevance, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.707-725, April 19-22, 1994
	12	Girard, J. Y. 1972. Interpretation fonctionelle et elimination des coupures dans l'aritmetique d'ordre superieur. Ph.D. thesis, Université Paris VII.
	13	Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
	14	J. Roger Hindley, Basic simple type theory, Cambridge University Press, New York, NY, 1997
	15	T. Jim, Rank 2 Type Systems and Recursive Definitions, Massachusetts Institute of Technology, Cambridge, MA, 1995
	16	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 [doi>10.1145/237721.237728]
	17	Jim, T. 2000. A polar type system. In ICALP Workshops. Proceedings in Informatics, vol. 8. Carleton-Scientific, 323--338.
	18	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, Type reconstruction in the presence of polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.290-311, April 1993 [doi>10.1145/169701.169687]
	19	A. J. Kfoury , J. B. Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order &lgr;-calculus, Proceedings of the 1994 ACM conference on LISP and functional programming, p.196-207, June 27-29, 1994, Orlando, Florida, United States
	20	A. J. Kfoury , J. B. Wells, Principality and decidable type inference for finite-rank intersection types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-174, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292556]
	21	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]
	22	Leporati, E. 2000. Intersezione al rank 2 per MiniOcaml. M.S.thesis, Dipartimento di Informatica, Università di Torino.
	23	Margaria, I. and Zacchi, M. 1995. Principal typing in a ∀∧ discipline. J. Logic Comp. 5, 367--381.
	24	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]
	25	Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
	26	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
	27	O'Caml. The O'Caml Language Home Page, http://www.ocaml.org.
	28	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	29	S. Ronchi Della Rocca, Principal type scheme and unification for intersection type discipline, Theoretical Computer Science, v.59 n.1-2, p.181-209, July 1988 [doi>10.1016/0304-3975(88)90101-6 ]
	30	Ronchi della Rocca, S. and Venneri, B. 1984. Principal Types Schemes for an extended type theory. Theoret. Comput. Sci. 28, 151--169.
	31	Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158702]
	32	Paweł Urzyczyn, Type reconstruction in F _ω, Mathematical Structures in Computer Science, v.7 n.4, p.329-358, August 1997 [doi>10.1017/S0960129597002302]
	33	van Bakel, S. 1993. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. Ph.D. thesis, Katholieke Universiteit Nijmegen.
	34	Steffen van Bakel , Franco Barbanera , Maribel Fernández, Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and beta-Rule, Selected papers from the International Workshop on Types for Proofs and Programs, p.41-60, June 12-16, 1999
	35	Wells, J. 1994. Typability and type-checking in the second-order lambda-calculus are equivalent and undecidable. In Logic in Computer Science. IEEE, 176--185.
	36	Hirofumi Yokouchi, Embedding a second-order type system into an intersection type system, Information and Computation, v.117 n.2, p.206-220, March 1995 [doi>10.1006/inco.1995.1040 ]

CITED BY 4

	Davide Ancona , Elena Zucca, Principal typings for Java-like languages, ACM SIGPLAN Notices, v.39 n.1, p.306-317, January 2004
	Peter Møller Neergaard , Harry G. Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Ferruccio Damiani, Rank 2 intersection types for modules, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.67-78, August 27-29, 2003, Uppsala, Sweden
	Sébastien Carlier , J. B. Wells, Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.132-143, August 24-26, 2004, Verona, Italy