On Isomorphism of "Functional'' Intersection and Union Types

ABSTRACT. Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the correct type. In presence of intersection and union types, type isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, which is quite complicated by the interference between functional and non functional types. The present paper faces this problem, by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This is done taking inspiration from the initial projection of Scott's inverse limit lambda-model. In particular, an isomorphism preserving reduction between types is defined. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, an interesting condition assuring isomorphism between types.