This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is well known that in the λ-calculus, independently of the considered type system, the isomorphism between two types can be realised only by invertible terms. Notably, all invertible terms are linear terms. In this paper, the isomorphism of intersection and union types is investigated using a relevant type system for linear terms enjoying the Subject Reduction property. To characterise type isomorphism, a similarity between types and a type reduction are introduced. Types have a unique normal form with respect to the reduction rules and two types are isomorphic if and only if their normal forms are similar.

In this paper we study the problem of finding a principal typing for a λ-term in a polymorphic intersection type assignment system. Following the approach of Coppo et al., Ronchi and Venneri, the principal type is proved to exist for any λ-term with a finite set of approximants. In the same way the existence of the principal type is shown for BCKλ-terms in a polymorphic type assignment system.