Principal Types as Partial Involutions
Furio Honsell, Marina Lenisa, Ivan Scagnetto
TL;DR
This work establishes a structural bridge between principal types in the affine $\lambda$-calculus and partial involutions in a Geometry of Interaction model. By developing an elementary type system for principal types and a corresponding model $\mathcal{I}$ of binary-type partial involutions, the authors show that GoI linear application coincides with unification-based resolution of principal types. They prove that closed affine terms interpret as partial involutions induced by their principal types and that the affine combinatory algebra $\mathcal{I}$ is a $\lambda$-algebra only on the linear fragment. The results answer Abramsky's open problem for the affine fragment and provide a conceptual, unifying view of GoI, principal types, and unification, with extensions to broader calculi and connections to other GoI models.
Abstract
We show that the principal types of the closed terms of the affine fragment of $λ$-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as partial involutions, in a natural Geometry of Interaction model à la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterising those partial involutions which are denotations of combinatory terms.