Intersection and Reference Types

Mariangiola Dezani-Ciancaglini
Dipartimento di Informatica, Università di Torino

Simona Ronchi della Rocca
Dipartimento di Informatica, Università di Torino

Abstract

Aim of this paper is to understand the interplay between intersection and reference types. Putting together the standard typing rules for intersection types and reference types leads to loss of sub ject reduction. The problem comes from the invariance of the reference type constructor and the rule of intersection elimination, which is essentially a subsumption rule. We propose a solution which only allows intersection of non-reference types, and in which the rule of intersection introduction uses an operator on types pushing intersections under references in an iterative way. The so obtained type assignment system is shown to be sound and, when restricted to pure lambda-calculus, as expressive as the standard type assignment system of intersection types.

Full text

PDF