The (In)Efficiency of Interaction

TL;DR

This paper investigates the efficiency trade-offs of interaction-based abstract machines for higher-order functional programs, revealing that their time inefficiency stems from higher-order types and providing a unified framework for analysis.

Contribution

It formulates four well-known abstract machines within a common framework to analyze their relative time efficiencies and links non-idempotent intersection types to these inefficiencies.

Findings

Interaction-based machines can be exponentially less efficient than environment-based ones.

Non-idempotent intersection types precisely reflect the time performance of the interactive machine.

Time inefficiency is primarily due to higher-order types.

Abstract

Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{time}$ performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how \emph{general} this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.