Structural Rules and Algebraic Properties of Intersection Types

TL;DR

This paper explores the algebraic and structural properties of intersection types, establishing connections between different intersection systems and their corresponding structural rules in type theory.

Contribution

It introduces notions of term expansion linking various intersection type systems with their structural properties and rules.

Findings

Relations between idempotent intersection and contraction

Connection of commutative intersection with exchange rule

Association of non-idempotent intersection with structural rules

Abstract

In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system, terms typed by non-idempotent intersections with terms typed in the affine and linear type systems and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. Finally, we show how idempotent intersection is related with the contraction rule, commutative intersection with the exchange rule and associative intersection with the lack of structural rules in a type system.