### Shin-ya Katsumata (RIMS, Kyoto, Japan), A Generic Soundness Result for Effect Systems

#### Schedule

- Feb. 13, 2012, 16:30 - 17:15

#### Abstract

Eﬀect system is a type-based approach to statically estimate side eﬀects caused by programs. Such estimation brings various beneﬁts to the analysis and transformation of programs. The purpose of the pioneering work by Lucassen and Giﬀord [5] was to design the eﬀect system that assists safe scheduling of expressions in parallel computing. Since then, eﬀect system has been widely applied to analysing the behaviour of programs. For instance, control ﬂow analysis can be concisely captured as an eﬀect system [6]. Region-based memory management in functional languages is developed based on the idea of eﬀect system [8]. A series of papers [3, 1, 2, 7] study a semantic foundation of some aggressive program transformations that depends on the results of eﬀect analysis.

The variety of eﬀect systems is governed by two factors. The ﬁrst factor is the side eﬀect implemented in a language, and the second factor is the property about side eﬀects that we estimate by an eﬀect system. Once we choose these factors, we aim to establish the eﬀect soundness, stating that when the eﬀect system asserts that a program P has an eﬀect e, the actual execution of P causes the side eﬀect that satisﬁes the property described by e.

This type of argument is common in many works on eﬀect system, but the eﬀect soundness is discussed in individual situations. This naturally leads us to seek for a general eﬀect soundness argument for any kind of side eﬀects. In this work we propose an eﬀect system and discuss the eﬀect soundness without committing into a particular computational eﬀect. The technical contributions are twofold:

- We design an eﬀect system with eﬀect polymorphism, and give a predicate semantics to it. The basic idea of this semantics is to interpret each type τ as a predicate over the eﬀect-erasure |τ|. To make the eﬀect system rich, we formulate eﬀects (with eﬀect variables) as morphisms in a discrete Lawvere Pos-theory containing the theory of monoid (1, ·). We use this monoid to represent the composition of eﬀects.

The key concept in the predicate semantics of the eﬀect system is the eﬀect-indexed lifting P of a monad A. It formulates Wadler and Thiemann’s eﬀect-delimited monad [9] in the context of predicate semantics. It maps a pair of an eﬀect e and a predicate X over I to a predicate P(e, X) over AI. Although P(e, −) is not a monad at each e, it collectively behaves as a monad when we move e inside the poset of eﬀects. The main axiom that guarantees this behaviour is that the multiplication µ of A maps the elements satisfying P(e, P(e′ , X)) into P(e · e′ , X).

- Typically, eﬀect soundness is discussed under a given description of eﬀects, which is formulated as a mapping from a pair of an eﬀect e and a type τ to a predicate D(e, τ) over the computation of type τ. The eﬀect soundness is then the claim that for any program M of type τ having an eﬀect e, the predicate semantics interprets M as an element in D(e, τ).

We present a method to construct an eﬀect-indexed lifting from a description of eﬀects. This construction is a variant of ⊤⊤-lifting [4] indexed by eﬀects. We then show that if 1) D(1, τ) contains all pure computations and 2) D is closed under generic eﬀects, then the constructed lifting gives a predicate semantics of the eﬀect system that is sound with respect to D. This result holds for a wide range of strong monads and descriptions of eﬀects.

**References**

[1] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for eﬀect- based program transformations with dynamic allocation. In M. Leuschel and A. Podelski, editors, PPDP, pages 87–96. ACM, 2007.

[2] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for eﬀect- based program transformations: higher-order store. In A. Porto and F. J. L´ pez-Fraguas, o editors, PPDP, pages 301–312. ACM, 2009.

[3] N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations. In N. Kobayashi, editor, APLAS, volume 4279 of Lecture Notes in Computer Science, pages 114–130. Springer, 2006.

[4] S. Katsumata. A semantic formulation of ⊤⊤-lifting and logical predicates for computa- tional metalanguage. In Proc. CSL ’05, volume 3634 of LNCS, pages 87–102. Springer, 2005.

[5] J. M. Lucassen and D. K. Giﬀord. Polymorphic eﬀect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’88, pages 47–57, New York, NY, USA, 1988. ACM.

[6] F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis (2. corr. print). Springer, 2005.

[7] J. Thamsborg and L. Birkedal. A kripke logical relation for eﬀect-based program transfor- mations. In M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors, ICFP, pages 445–456. ACM, 2011.

[8] M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In POPL, pages 188–201, 1994.

[9] P. Wadler and P. Thiemann. The marriage of eﬀects and monads. ACM Trans. Comput. Log., 4(1):1–32, 2003.