With or Without You: Programming with Effect Exclusion
summary
A new Hindley‑Milner style type-and-effect system adds union, intersection and complement to express “any effects except these” and implements effect exclusion as a first‑class construct; it formalizes this in the λ∁ calculus, proves progress, preservation and an effect‑safety theorem that “no excluded effect is ever performed,” extends Algorithm W with Boolean unification for complete inference, ships as a Flix extension of 10,000 lines of code, and is evaluated on 59 program fragments with two runnable proofs‑of‑concept (GUI non‑blocking and an effect‑parametric event bus).
AI-written summary · about
chapters (17)
- 0:00Effect exclusion research
- 1:53Effect exclusion in real code
- 4:00Limitations of effect systems
- 5:24Effect exclusion examples
- 7:10Vulnerabilities prevented
- 8:12Formalizing in Lambda calculus
- 13:51Flix implementation
- 14:34Case studies evaluation
- 16:19GUI and event bus libraries
- 18:03Conclusion and future
- 19:11Q&A: Tail calls
- 19:57Q&A: User study
- 20:19Q&A: Boolean unification
- 21:24Q&A: Boolean complexity
- 22:08Q&A: Effect polymorphism
- 24:14Q&A: Row-based systems
- 26:02Q&A: Effect granularity
related talks
14mFundamentalist Functional Programming
46mFunctional effects in perspective
50mFunctional Programming with Effects
43mFunctional Programming with Effects
33mRethinking Effects with Effect Systems
44mEffects, Algebraically yours ..
33mExtensible Effects: A Leaner Cake for Purely Functional Code
27mLimiting side-effects of applications at compile-time