Recovering Purity with Comonads and Capabilities
summary
A call-by-value impure lambda calculus is extended with a comonadic safety modality that tags variables as safe or impure and a box comonad that internalizes capability safety; a capability space model gives a denotational semantics in a cartesian closed category with a monad and interacting comonad. The paper proves substitution and equational (call-by-value β and η) soundness, shows map1 and map2 become provably equal when passed pure (boxed) functions, and embeds STLC with beta-eta preservation.
AI-written summary · about
chapters (6)
related talks
26mTemporal refinements for Call-By-Push-Value with fixpoint
30mContinuations and Coexponentials
17mNotions of Stack-manipulating Computation and Relative Monads
15mMonadic Compiler Calculation (Functional Pearl)
49mSemantic Foundations for Probabilistic Programming
17mMonadic and Comonadic Aspects of Dependency Analysis
15mMonadification of Attribute Grammars
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)