Isomorphism of intersection and union types

摘要

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