Principal types as partial involutions

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 characterizing those partial involutions which are denotations of combinatory terms.