Effect の双対、Coeffect

昨今巷で Effect システムが流行っていますが、実はその双対、Coeffect システムというものがあるのをご存じでしょうか。
Effect が関数のボディでの作用について述べるシステムだとすれば、Coeffect は対称的に、引数の性質について述べるシステムです。変数の使用回数のトラッキング、セキュリティレベルの追跡などがそのインスタンスになることが知られています。

Effect システムについても軽く説明しますが、型付きラムダ計算等の知識は前提とします。

Transcript

1. Coeffect System ゆきくらげ @yukikurage_2019 Effect の双対、Coeffect #fp_matsuri_a 2025.06.14
2. Who’s YUKIKURAGE (in 30 sec.) Coeffect System 2 2003 : BIRTH 2003~2025 : ALIVE 🐦 Twitter : yukikurage_2019 🌟 Fav : Haskell, PureScript 🎮 Fav game : Slay the Spire / Music & Illustrations / Games / Web Applications NO IMAGE
3. Agenda Coeffect System 3 #1 Background: Effect System #2 Coeffect System #3 Where is the “Duality”?
4. Background: Effect System #1
5. Pure Computation Coeffect System #1 Background: Effect System 5 - Just takes a value and returns a value - No “Side Effects” - Has ref. transparency - No effect on the environment fun f(a) = b <- a + 2 c <- b * 3 return c - 4
6. But we want to use… Coeffect System #1 Background: Effect System 6 fun f(a) = b <- get() set(a * b) Global States fun f(a) = log(a) return a + 1 Logging fun f(a) = b <- random() return a + b Random Value … while keeping away from pure computation
7. Simple Idea: Type Annotation Coeffect System #1 Background: Effect System 7 Computation using random values → t & {RAND} fun f(a : int) : int & {RAND} = b <- random() return a + b
8. Simple Idea: Type Annotation Coeffect System #1 Background: Effect System 8 Computation that outputs logs → t & {LOG} fun f(a : int) : int & {LOG} = log(a) return a + 1
9. Simple Idea: Type Annotation Coeffect System #1 Background: Effect System 9 And both! → t & {RAND, LOG} fun f(a : int) : int & {RAND, LOG} = b <- random() log(a) return a + b
10. Simple Idea: Type Annotation Coeffect System #1 Background: Effect System 10 Pure Computation → t & {} fun f(a : int) : int & {} = b <- a + 2 c <- b * 3 return c - 4 → We can know purity of computation
11. How is this possible? Coeffect System 11 #1 Background: Effect System
12. Effect Composing Coeffect System #1 Background: Effect System 12 Γ ⊦ c1 : σ Δ, x : σ ⊦ c2 : τ Γ, Δ ⊦ (x ← c1 ; c2 ) : τ Current computation Continuation Composed computation
13. Effect Composing Coeffect System #1 Background: Effect System 13 Γ ⊦ c1 : σ & e1 Δ, x : σ ⊦ c2 : τ & e2 Γ, Δ ⊦ (x ← c1 ; c2 ) : τ & e1 ∪ e2 Current effects Effects of the continuation Composed effects
14. Pure comp. / Effect expansion Coeffect System #1 Background: Effect System 14 Γ ⊦ v : τ Γ ⊦ (return v) : τ & ∅ Pure computation Γ ⊦ c : τ & e1 Γ ⊦ c: τ & e2 Effect expansion e1 ⊆ e2
15. Now, Time to … Coeffect System 15 #2 Coeffect System
16. Generalize! Coeffect System 16 #2 Coeffect System
17. Time to generalize! Coeffect System #1 Background: Effect System 17 Ω : Set of all effects Effect calcs (Ω, ∅, ∪, ⊆) Monoid (M, 1M , ×M , ≤M )
18. The (Generalized) Effect System Coeffect System #1 Background: Effect System 18 Γ ⊦ c1 : σ & e1 Δ, x : σ ⊦ c2 : τ & e2 Γ, Δ ⊦ (x ← c1 ; c2 ) : τ & e1 ×M e2 Γ ⊦ v : τ Γ ⊦ (return v) : τ & 1M Γ ⊦ c : τ & e1 Γ ⊦ c: τ & e2 e1 ≤M e2 compose pure subs
19. Coeffect System #2
20. Motivation Coeffect System #2 Coeffect System 20 How we know about “contexts” of expressions
21. Ex 1 : Max usage count Coeffect System #2 Coeffect System 21 Type systems that tracks the maximum number of arguments used fun f(a @ 2) = a + a → Argument “a” can be used up to twice fun g(a @ 3, b @ 2) = f(a) + f(b) + a
22. Ex 2 : Security tracking Coeffect System #2 Coeffect System 22 Type systems that tracks the security level of arguments fun f(a @ public, b @ private) = send(a) → Argument “a” can be sent, while “b” cannot fun f(a @ public, b @ private) = send(b) → Type Error!
23. Typing of Max usage count Coeffect System #2 Coeffect System 23 x1 : σ1 , … xk : σk ⊦ e : τ x1 : σ1 , … xk : σk @ n1 , … nk ⊦ e : τ Let's annotate Context!
24. Typing of Max usage count Coeffect System #2 Coeffect System 24 x1 : σ1 , … xk : σk @ n1 , … nk ⊦ e : τ "We can obtain the value of expression e provided that x1 may be used n1 times, x2 n2 times, and so on." means …
25. Typing of Max usage count Coeffect System #2 Coeffect System 25 Γ @ R ⊦ e1 : σ Δ, x : σ @ S, n ⊦ e2 : τ Γ, Δ @ R × n, S ⊦ (x ← e1 ; e2 ) : τ e2 can be obtained from n copies of x. ...so we need n copies of Γ We can get e1 from context Γ
26. Typing of Max usage count Coeffect System #2 Coeffect System 26 Γ, x : σ, y : σ @ R, n, m ⊦ e2 : τ Γ, z : σ @ R, n + m ⊦ e2 [x, y ↦ z]: τ x + y x : σ @ 1, y : σ @ 1 ⊦ z + z z : σ @ 2 ⊦ Splitting the values within the environment (unlike effect typing)
27. Typing of Max usage count Coeffect System #2 Coeffect System 27 x : τ @ 1 ⊦ x : τ Variable Γ, x : σ @ R, n ⊦ e : τ Max bound n ≦ m Γ, x : σ @ R, 0 ⊦ e : τ No use Γ @ R ⊦ e : τ Γ, x : σ @ R, m ⊦ e : τ
28. Now, Time to … Coeffect System 28 #2 Coeffect System
29. Generalize! Coeffect System 29 #2 Coeffect System
30. Time to generalize Coeffect System #2 Coeffect System 30 Nat semiring (ℕ, 0, +, 1, ×, ≤) Semiring (S, 0S , +S , 1S , ×S , ≤S )
31. The Coeffect System Coeffect System #1 Background: Effect System 31 Γ @ R ⊦ e1 : σ Δ, x : σ @ S, n ⊦ e2 : τ Γ, Δ @ R ×S n, S ⊦ (x ← e1 ; e2 ) : τ compose Γ, x : σ, y : σ @ R, n, m ⊦ e2 : τ Γ, z : σ @ R, n +S m ⊦ e2 [x, y ↦ z]: τ split x : τ @ 1S ⊦ x : τ Variable Γ , x : σ @ R, 0S ⊦ e : τ Ignore Γ @ R ⊦ e : τ Γ, x : σ @ R, n ⊦ e : τ Max bound n ≦S m Γ, x : σ @ R, m ⊦ e : τ
32. Instance : Security tracking Coeffect System #1 Background: Effect System Γ @ R ⊦ e1 : σ Δ, x : σ @ S, n ⊦ e2 : τ Γ, Δ @ max(R, n), S ⊦ (x ← e1 ; e2 ) : τ x : τ @ 0 ⊦ x : τ Default is private Instantiate by semiring ({0, 1}, 0, max, 1, min, ≦) where 0 = private, 1 = public Apply the most weak (max) security 32
33. Where is the “Duality” #3
34. Categorical Semantics Coeffect System #3 Where is the “Duality” Category = Objects linked by arrows A B C f g h idB idC idA 34
35. Categorical Semantics Coeffect System #3 Where is the “Duality” Object : type Arrows : function Int String 35 Bool A function from Int to String
36. Duality Coeffect System #3 Where is the “Duality” Category Cop : Objects : objects in C Arrows : reversed C arrows A B C f g h A B C fop gop hop Category C Category Cop 36
37. Duality Coeffect System #3 Where is the “Duality” Dual of X in category C (often called Co-X) is X in category Cop 37 Simply put… Co-X is X, but arrows are reversed
38. Cat Semantics of Effect Coeffect System #3 Where is the “Duality” 38 (Strong-) Graded Monad Γ M(σ) M(τ) σ Γ M(τ) Monad M Γ ⊦ c1 : σ & e1 Δ, x : σ ⊦ c2 : τ & e2 Γ, Δ ⊦ (x ← c1 ; c2 ) : τ & e1 ×M e2 effect composition
39. Comonad Coeffect System #3 Where is the “Duality” 39 A M(B) M(C) B A M(C) Monad M B W(A) W(B) C C W(A) Comonad W DUAL!
40. Cat Semantics of Coeffect Coeffect System #3 Where is the “Duality” 40 (Exponential-) Graded Comonad B W(A) W(B) C C W(A) Comonad W Γ @ R ⊦ e1 : σ Δ, x : σ @ S, n ⊦ e2 : τ Γ, Δ @ R ×S n, S ⊦ (x ← e1 ; e2 ) : τ coeffect composition
41. Where is the duality Coeffect System #3 Where is the “Duality” Effect System 41 Graded Strong Monad Coeffect System Graded Exponential Comonad Dual Categorical Semantics
42. Intuition Coeffect System #3 Where is the “Duality” 42 Γ ⊦ c : τ & e @ e Effect System Coeffect System
43. (APPENDIX) Where is the semiring from? Coeffect System #3 Where is the “Duality” 43 (Near-) Semiring : ＋ is commutative monoid × is monoid (a ＋ b) × c = (a × c) ＋ (b × c) ← ???
44. Where is the semiring from? Coeffect System #3 Where is the “Duality” 44 Function Composition A f g g . f B C
45. Where is the semiring from? Coeffect System #3 Where is the “Duality” 45 Context merging A f g f ⊗ g B C B ⊗ C (Tuple of B and C)
46. Where is the semiring from? Coeffect System #3 Where is the “Duality” 46 A f g B C D C ⊗ D h g ⊗ h (g ⊗ h) . f
47. Where is the semiring from? Coeffect System #3 Where is the “Duality” 47 A f g g . f B C D C ⊗ D h h . f (g . f) ⊗ (h . f)
48. Where is the semiring from? Coeffect System #3 Where is the “Duality” 48 A f g g . f B C D C ⊗ D h h . f g ⊗ h (g ⊗ h) . f ~ (g . f) ⊗ (h . f) (g ⊗ h) . f ~ (g . f) ⊗ (h . f)
49. Summary Coeffect System 49 - Coeffect System - is generalized typing system, which - can use “context” information - is (almost) dual of Effect system
50. References Coeffect System 50 Petricek, T., Orchard, D., & Mycroft, A. “Coeffects: Unified Static Analysis of Context- Dependence”. ICALP 2013. Petricek, T., Orchard, D., & Mycroft, A. “Coeffects: a calculus of context-dependent computation”. ACM SIGPLAN Notices, Vol. 49. Gaboardi, M., Katsumata, S., Orchard, D., Breuvart, F., & Uustalu, T. “Combining effects and coeffects via grading”. ICFP 2016. Sanada, T. “Category-Graded Algebraic Theories and Effect Handlers”. Electronic Notes in Theoretical Informatics and Computer Science, Vol. 1 (February 2023). DOI: 10.46298/entics.10491. Fukihara, Y., & Katsumata, S. "Generalized Bounded Linear Logic and its Categorical Semantics". FOSSACS 2021