Coeffects for Sharing and Mutation
summary
Coeffects model sharing in a Java-like calculus by representing effects as sets-of-links coeffects with a distinguished res link for result aliasing and applying a transitive-closure after pointwise combination to capture non‑structural sharing. The type system encodes promotions (read/capsule/immutable), types clone/mix examples precisely, and proves soundness via subject reduction plus preservation of capsule encapsulation and immutability of graphs. Works on realistic examples that other systems struggle with and yields more compact, compositional rules.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:34Coeffect judgment
- 1:04A simple example
- 2:55Adding coeffects: typing rules
- 4:16Structure of coeffects
- 6:07Existing systems: uniqueness and immutability
- 8:06Sharing (formally in our calculus)
- 16:17The clone example in action
- 17:50Expressive power
- 18:38Can we model sharing by coeffects?
- 19:17Key idea (1): coeffects are sets of links
- 20:14Key idea (2): operations on coffect contexts apply closure
- 20:46The sharing coeffect system
- 21:57Selected typing rules: field assign
- 22:53Selected typing rules: promotion (simplified version)
- 24:12Capsule and immutable properties
related talks
29mLogical Relations for Effect Capabilities
19mAssociated Effects: Flexible Abstractions for Effectful Programming
14mAdequacy for Algebraic Effects Revisited
15mHandling Bidirectional Control Flow
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
11mLocal algebraic effect theories
45mA categorical view of computational effects