Memoryful Geometry of Interaction - group-mmm.org

1 Memoryful Geometry of Interaction From Coalgebraic Components to Algebraic Effects Naohiko Hoshino Koko Muroya ichiro Hasuo RIMS, Kyoto University Dept. Computer Science, University of Tokyo Abstract ematical counterpart of control flow in program execution, and in Girard's Geometry of Interaction (GoI) is Interaction based seman- this way, GoI connects mathematics (denotational semantics), pro- tics of linear logic proofs and, via suitable translations, of func- gram evaluation (operational semantics) and state based computa- tional programs in general. Its mathematical cleanness identifies tion (low-level languages/implementations).

2 Applications of GoI. essential structures in computation; moreover its use as a compila- are widespread: implementation of (imperative) functional pro- tion technique from programs to state machines GoI implemen- gramming languages [8, 9, 25]; relationship to Krivine abstract tation, so to speak has been worked out by Mackie, Ghica and machines [7] and to defunctionalization [30]; optimal graph reduc- others. In this paper, we develop Abramsky's idea of resumption tion for the lambda calculus [11]; and the design of a functional based GoI systematically into a generic framework that accounts programming language for sublinear space [6].

3 For computational effects (nondeterminism, probability, exception, Categorical GoI. global states, interactive I/O, etc.). The framework is categorical: Plotkin & Power's algebraic operations provide an interface to This remarkable level of integration in GoI of operational and computational effects; the framework is built on the categorical ax- denotational/structural semantics is further exemplified by its iomatization of GoI by Abramsky, Haghverdi and Scott; and, by categorical axiomatics (categorical GoI) developed by Abramsky, use of the coalgebraic formalization of component calculus, we de- Haghverdi and Scott [2]. There a general construction is given from scribe explicit construction of state machines as interpretations of a traced monoidal category together with additional constructs, functional programs.

4 The resulting interpretation is shown to be altogether called a GoI situation to a combinatory algebra. One sound with respect to equations between algebraic operations, as can then apply the realizability construction (see [24]) that well as to Moggi's equations for the computational lambda calcu- turns a combinatory algebra (an untyped model) into a categori- lus. We illustrate the construction by concrete examples. cal model of a typed calculus, from which one extracts realizers as concrete interpretations. The latter are sound by construction. Categories and Subject Descriptors [Formal Definitions and In a big picture, the current work is one of the attempts to instan- Theory]: Semantics; [Semantics of Programming Languages]: tiate this general methodology of categorical GoI to concrete situ- Algebraic approaches to semantics ations.

5 Our starting point is the previous work [14] where we ex- General Terms Theory tend the above workflow by a step prior to it. The extension comes from the following observation (a folklore result, see Lemma ;. Keywords Geometry of Interaction , monad, algebraic effect see also [18]): many traced monoidal categories arise as a Kleisli category of a monad with a suitable order structure. The resulting 1. Introduction extended workflow is as follows. Geometry of Interaction (GoI) is introduced by Girard [10] as (a Set-monad T whose Kleisli category is Cppo-enriched). Kleisli construction semantics of proofs programs, under the Curry-Howard 7 (a traced monoidal category).

6 Correspondence for the study of dynamics and invariants of the categorical GoI [2]. 7 (a combinatory algebra) (1). cut elimination process ( program execution). Girard's original realizability &. presentation of GoI is in the language of C -algebras; Mackie's realizer extraction alternative presentation [25] as token machines initiated another 7 (a GoI interpretation of a typed calculus). important application of GoI, namely as a compilation technique. There GoI provides translation of programs into state machines; In [14] we pursued use of this extended general workflow that is and the machines' execution results are invariant under cut elimi- parametrized by T : in order to interpret a calculus with a certain nation.

7 Dynamics in such machines can be understood as a math- additional feature, we start with a monad T equipped with the same feature, and the generic constructions would yield a suitable GoI. interpretation. In [14], specifically, we considered a calculus for quantum computation. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation Effects and Resumption Based GoI. on the first page. Copyrights for components of this work owned by others than ACM However, following this naive scenario turned out to be far from must be honored.

8 Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a straightforward: in [14] we ended up using a complicated continu- fee. Request permissions from ation monad that keeps track of all the measurement outcomes. In CSL-LICS 2014, July 14 18, 2014, Vienna, Austria. fact the same kind of difficulty is already with nondeterminism . Copyright c 2014 ACM 978-1-4503-2886-9.. $ one of the most basic computational effects as we exhibit now. Here we shall speak on the intuitive level, using the game-theoretic terms of queries and answers instead of the categorical language Plotkin & Power [28].

9 Concrete interpretations are given by (state for GoI. based) transducers with the same effect T , much like the non- Consider the call-by-value evaluation of the program deterministic one in (3). Assuming that T comes with a suitable Cppo structure many effects qualify by the slight modification ( x : nat. x + x) (0 t 1) (2) of adding partiality we show that the category Res(T ) of T - where the subterm 0 t 1 returns 0 or 1 nondeterministically. Then resumptions is traced monoidal. Then the general workflow in (1), the whole program is expected to return 0 or 2. However, the usual starting from its second step, yields a GoI interpretation of a cal- GoI interpretation of (2) may return an unexpected value 1, as the culus, with transducers as realizers.

10 The resulting interpretation result of the following Interaction . is sound with respect to the algebraic axioms ( associativity of t) as well as Moggi's equations for the computational lambda 1. We ask the value of the left occurrence of x in x + x. calculus. 2. The subterm 0 t 1 answers 0 or 1 nondeterministically. This overall procedure from a monad T and algebraic opera- tions to a GoI interpretation in the form of T -transducers we wish 3. We ask the value of the right occurrence of x in x + x. to call Memoryful GoI, emphasizing the role of memories ( mem- 4. The subterm 0 t 1 answers 0 or 1 nondeterministically. ories here are the same as internal states ; the choice is to dis- 5.)