Rank 2 intersection types for modules

ABSTRACT

We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for the module language. We first consider a "plain" notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrate the notions of: module intrachecking (each module is typechecked in isolation and its interface, which is the set of typings of the defined identifiers, is inferred); interface interchecking (when linking modules, typechecking is done just by looking at the interfaces); interface specialization (interface intrachecking may require to specialize the typing listed in the interfaces); principal interfaces (the principal typing property for the type system of modules); and separate typechecking (looking at the code of the modules does not provide more type information than looking at their interfaces). Then we illustrate some limitations of the "plain" framework and extend the module language and the type system in order to overcome these limitations. The decidability of the system is shown by providing algorithms for the fundamental operations involved in module intrachecking and interface interchecking.

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: H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48:931--940, 1983.
• 3: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 4: 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
• 5: M. Coppo and M. Dezani-Ciancaglini. An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685--693, 1980.
• 6: M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional Characters of Solvable Terms. Zeith. Math. Logik Und Grund. Math., 27:45--58, 1981.
• 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: L. M. M. Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1984.
• 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: F. Damiani. Rank 2 Intersection Types for Modules. Version with conclusions and appendices - available at: http://www.di.unito.it/~damiani/papers/ppdp03.html.
• 11: 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 [doi>10.1145/778559.778560]
• 12: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• 13: J. Roger Hindley, Basic simple type theory, Cambridge University Press, New York, NY, 1997
• 14: 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]
• 15: 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]
• 16: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 17: 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]
• 18: S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.
• 19: J. B. Wells, The Essence of Principal Typings, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, p.913-925, July 08-13, 2002
• 20: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages; Recursion; Polymorphism

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs; Type structure

General Terms:
Algorithms, Languages, Theory

Keywords:
principal typings, separate compilation, type inference