Università di Torino

Research on "Formal Methods in Computing"

Rank 2 intersection types for local definitions and conditional expressions

(Supersedes the paper [Damiani, 2000] )

Ferruccio DAMIANI

ABSTRACT. We introduce 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 typing), 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 be useful also for other type systems.
An on-line demostration of a prototype implementation of the type system presented in the paper is available.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


   author    = {F. Damiani},
   title     = {Rank 2 intersection types for local definitions and
                conditional expressions},
   journal   = {ACM Transactions On Programming Languages and Systems},
   year      = {2003},
   volume    = {25},
   number    = {4},
   pages     = {401--451},
   publisher = {ACM}

["Formal Methods in Computing" group] [Department's HOME]

Last update: Mar 14, 2007