Toward Isomorphism of Intersection and Union types

Abstract

This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. 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, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types.