Rank 2 Intersection for Recursive Definitions

• Autorzy: Damiani F.
• Języki publikacji: EN

Abstrakty

EN

Let |- be an intersection type system. We say that a term is |--simple (or just simple when the system |- is clear from the context) if system |- can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (non-simple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems.

Słowa kluczowe

EN

type inference; principal typings; polymorphic recursion

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 451--488
• Opis fizyczny: bibliogr. 24 poz.

Twórcy

autor

Damiani F.

• Dipartimento di Informatica, Universita di Torino, c.Svizzera 185, I-10149 Torino, Italy,

Bibliografia

• [1] van Bakel, S.: Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems, Ph.D. Thesis, Katholieke Universiteit Nijmegen, 1993.
• [2] van Bakel, S.: Rank 2 types for term graph rewriting, TIP'02, ENTCS 75, Elsevier, 2003.
• [3] Barendregt, H. P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment, J. of Symbolic Logic, 48, 1983, 931-940.
• [4] Carlier, S., Polakow, J., Wells, J. B., Kfoury, A. J.: System E: Expansion variables for flexible typing with linear and non-linear types and intersection types., ESOP'04, LNCS 2986, Springer, 2004.
• [5] Coppo, M.: An extended polymorphic type system, MFCS'80, LNCS 88, Springer, 1980.
• [6] Coppo, M., Dezani-Ciancaglini, M.: An extension of basic functional theory for lambda-calculus, Notre Dame Journal of Formal Logic, 21(4), 1980, 685-693.
• [7] Cousot, P.: Types as abstract interpretations, POPL'97, ACM, 1997.
• [8] Damas, L. M. M., Milner, R.: Principal type schemas for functional programs, POPL'82, ACM, 1982.
• [9] Damiani, F.: Rank 2 intersection types for local definitions and conditional expressions, ACM Trans. Prog. Lang. Syst., 25(4), 2003, 401-451.
• [10] Damiani, F.: Rank-2 intersection and polymorphic recursion, TLCA'05, LNCS 3461, Springer, 2005.
• [11] Gori, R., Levi, G.: Properties of a type abstract interpreter, VMCAI'03, LNCS 2575, Springer, 2003.
• [12] Hallett, J. J., Kfoury, A. J.: Programming examples needing polymorphic recursion, ITRS'04 (workshop affiliated to LICS'04), ENTCS 136, Elsevier, 2005.
• [13] Henglein, F.: Type inference with polymorphic recursion, ACM Trans. Prog. Lang. Syst., 15(2), 1993, 253-289.
• [14] Hindley, R.: Basic Simple Type Theory, Number 42 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1997.
• [15] Jim, T.: Rank 2 type systems and recursive definitions, Technical Report MIT/LCS/TM-531, LCS, Massachusetts Institute of Technology, 1995.
• [16] Jim, T.: What are principal typings and what are they good for?, POPL'96, ACM, 1996.
• [17] Jim, T.: A polar type system, ICALP Workshops, 8, Carleton-Scientific, 2000.
• [18] Kfoury, A. J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion, ACM Trans. Prog. Lang. Syst., 15(2), 1993, 290-311.
• [19] Leivant, D.: Polymorphic type inference, POPL'83, ACM, 1983.
• [20] Meertens, L.: Incremental polymorphic type checking in B, POPL'83, ACM, 1983.
• [21] Mycroft, A.: Polymorphic type schemes and recursive definitions, International Symposium on Programming, LNCS 167, Springer, 1984.
• [22] Terauchi, T., Aiken, A.: On typability for polymorphic recursive rank-2 intersection types, LICS'06, IEEE, 2006.
• [23] Wells, J.: The essence of principal typings, ICALP'02, LNCS 2380, Springer, 2002.
• [24] Yokouchi, H.: Embedding a second-order type system into an intersection type system, Information and Computation, 117, 1995, 206-220.