Research on "Formal Methods in Computing"

Rank 2 intersection types for local definitions and conditional expressions

(Supersedes the paper [Damiani, 2000] )

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.

• pdf ( © ACM, 2003 ).

BIBTEX.

@article{Damiani:TOPLAS-2003,
   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}
}