Shin-ya Katsumata (RIMS, Kyoto, Japan), A Generic Soundness Result for Effect Systems
Schedule
- Feb. 13, 2012, 16:30 - 17:15
Abstract
Effect system is a type-based approach to statically estimate side effects caused by programs. Such estimation brings various benefits to the analysis and transformation of programs. The purpose of the pioneering work by Lucassen and Gifford [5] was to design the effect system that assists safe scheduling of expressions in parallel computing. Since then, effect system has been widely applied to analysing the behaviour of programs. For instance, control flow analysis can be concisely captured as an effect system [6]. Region-based memory management in functional languages is developed based on the idea of effect 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 effect analysis.
The variety of effect systems is governed by two factors. The first factor is the side effect implemented in a language, and the second factor is the property about side effects that we estimate by an effect system. Once we choose these factors, we aim to establish the effect soundness, stating that when the effect system asserts that a program P has an effect e, the actual execution of P causes the side effect that satisfies the property described by e.
This type of argument is common in many works on effect system, but the effect soundness is discussed in individual situations. This naturally leads us to seek for a general effect soundness argument for any kind of side effects. In this work we propose an effect system and discuss the effect soundness without committing into a particular computational effect. The technical contributions are twofold:
- We design an effect system with effect polymorphism, and give a predicate semantics to it. The basic idea of this semantics is to interpret each type τ as a predicate over the effect-erasure |τ|. To make the effect system rich, we formulate effects (with effect variables) as morphisms in a discrete Lawvere Pos-theory containing the theory of monoid (1, ·). We use this monoid to represent the composition of effects.
The key concept in the predicate semantics of the effect system is the effect-indexed lifting P of a monad A. It formulates Wadler and Thiemann’s effect-delimited monad [9] in the context of predicate semantics. It maps a pair of an effect 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 effects. 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, effect soundness is discussed under a given description of effects, which is formulated as a mapping from a pair of an effect e and a type τ to a predicate D(e, τ) over the computation of type τ. The effect soundness is then the claim that for any program M of type τ having an effect e, the predicate semantics interprets M as an element in D(e, τ).
We present a method to construct an effect-indexed lifting from a description of effects. This construction is a variant of ⊤⊤-lifting [4] indexed by effects. We then show that if 1) D(1, τ) contains all pure computations and 2) D is closed under generic effects, then the constructed lifting gives a predicate semantics of the effect system that is sound with respect to D. This result holds for a wide range of strong monads and descriptions of effects.
References
[1] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-
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 effect-
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. Gifford. Polymorphic effect 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 effect-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 effects and monads. ACM Trans. Comput.
Log., 4(1):1–32, 2003.
Effect system is a type-based approach to statically estimate side effects caused by programs. Such estimation brings various benefits to the analysis and transformation of programs. The purpose of the pioneering work by Lucassen and Gifford [5] was to design the effect system that assists safe scheduling of expressions in parallel computing. Since then, effect system has been widely applied to analysing the behaviour of programs. For instance, control flow analysis can be concisely captured as an effect system [6]. Region-based memory management in functional languages is developed based on the idea of effect 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 effect analysis.
The variety of effect systems is governed by two factors. The first factor is the side effect implemented in a language, and the second factor is the property about side effects that we estimate by an effect system. Once we choose these factors, we aim to establish the effect soundness, stating that when the effect system asserts that a program P has an effect e, the actual execution of P causes the side effect that satisfies the property described by e.
This type of argument is common in many works on effect system, but the effect soundness is discussed in individual situations. This naturally leads us to seek for a general effect soundness argument for any kind of side effects. In this work we propose an effect system and discuss the effect soundness without committing into a particular computational effect. The technical contributions are twofold:
- We design an effect system with effect polymorphism, and give a predicate semantics to it. The basic idea of this semantics is to interpret each type τ as a predicate over the effect-erasure |τ|. To make the effect system rich, we formulate effects (with effect variables) as morphisms in a discrete Lawvere Pos-theory containing the theory of monoid (1, ·). We use this monoid to represent the composition of effects.
The key concept in the predicate semantics of the effect system is the effect-indexed lifting P of a monad A. It formulates Wadler and Thiemann’s effect-delimited monad [9] in the context of predicate semantics. It maps a pair of an effect 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 effects. 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, effect soundness is discussed under a given description of effects, which is formulated as a mapping from a pair of an effect e and a type τ to a predicate D(e, τ) over the computation of type τ. The effect soundness is then the claim that for any program M of type τ having an effect e, the predicate semantics interprets M as an element in D(e, τ).
We present a method to construct an effect-indexed lifting from a description of effects. This construction is a variant of ⊤⊤-lifting [4] indexed by effects. We then show that if 1) D(1, τ) contains all pure computations and 2) D is closed under generic effects, then the constructed lifting gives a predicate semantics of the effect system that is sound with respect to D. This result holds for a wide range of strong monads and descriptions of effects.
References
[1] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect- 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 effect- 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. Gifford. Polymorphic effect 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 effect-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 effects and monads. ACM Trans. Comput. Log., 4(1):1–32, 2003.