Representing permutations without permutations, or the expressive power of sequence types

TL;DR

This paper demonstrates that a rigid, permutation-free type system can fully represent the expressive power of more flexible systems that include permutations, capturing all reduction behaviors.

Contribution

It proves that permutation-free coinductive type systems can express all behaviors of systems allowing permutations, showing full expressive power.

Findings

Permutation-free derivations can represent all non-idempotent derivations.

Dynamic behaviors are fully captured without permutations.

Rigid systems have the same expressive power as permutation-inclusive systems.

Abstract

Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on e.g., typing derivations. We previously introduced a very constrained coinductive type system (system S) in which permutation is completely disallowed. One may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one allowing permutations. We answer this question in the most general case i.e. coinductive type grammars without validity conditions. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S has full expressive power over multiset/permutation-inclusive intersection.