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.

• ps , ps.gz

BIBTEX.

@techreport{Damiani:TR-01,
   author    = {F. Damiani},
   title     = {Rank 2 intersection types for local definitions and
                conditional expressions},
   institution = {Dipartimento di Informatica, Universit\`a di Torino},
   number    = {TR 63/01},
   year      = {2001}
}