Toward Isomorphism of Intersection and Union types

TL;DR

This paper explores the properties of type isomorphism in a lambda-calculus with intersection and union types, establishing a normal form-based characterization of when types are isomorphic.

Contribution

It introduces a type reduction system with confluence and termination, and characterizes type isomorphism via normal forms in a lambda-calculus with intersection and union types.

Findings

Types with the same normal form are isomorphic

Type reduction is confluent and terminating

Normal forms enable complete characterization of type isomorphism

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.