Affect: An Affine Type and Effect System
summary
Affect introduces Affine types to statically distinguish one-shot versus multi-shot effect continuations, implements a small language called Affect with ML references and effect handlers, and mechanizes a semantic type-soundness proof via a logical relation in Iris/Coq. It adapts Rust’s Cell-like references and Wadler’s use types to allow storing one-shot continuations safely (replace API) and to support bounded polymorphism; a concrete counterexample shows a common optimization turning UNO into DUO changes collect_all’s result from [false, true] to [false, false], so the system enforces at-most-once resumption and comes with reusable artifacts.
AI-written summary · about