Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects

ABSTRACT. Girard's Geometry of Interaction (GoI) is interaction-based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state-based machines has been worked out by Mackie, Ghica and others. In this paper, we take Abramsky's idea of resumption-based GoI and develop it systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: algebraic operations provide an interface to computational effects (following Plotkin and Power); the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, the framework describes explicit construction of state machines as interpretations of functional programs. The obtained models are shown to be sound with respect to equations between algebraic operations, as well as to Moggi's standard equations for the computational lambda calculus. The construction is illustrated by concrete examples.