Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
summary
A new language called Effekt implements contextual effect polymorphism by making function-like blocks second class so they cannot escape, providing a proof-backed type system and an interactive REPL. Effect annotations drive operational behavior and are translated to capability-passing style, so types guarantee handlers are lexical and prevent accidental capture. Examples show different annotations produce concrete results (examples yield 42 vs 84). Trade-offs include no first-class functions and that an empty effect set does not imply global purity.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:10Parametric Effect Polymorphism
- 2:50You do not talk about effect polymorphism!
- 4:38Contextual Effect Polymorphism
- 6:19Second-Class Values in Effekt
- 8:22Lexical Scoping of Handlers
- 9:24Contextual Reading
- 9:50Purity
- 10:19Operational Semantics
- 11:12Capability-Passing Style
- 12:40Effect Encapsulation: Multicore OCaml
- 12:53Effect Encapsulation: Koka & Frank
- 13:45Effect Encapsulation: Effekt
- 14:18Conclusion
related talks
12mCompiling Effect Handlers in Capability-Passing Style
32mHigh-Level Effect Handlers in C++
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
51mEffects: to be or not to be?
29mLogical Relations for Effect Capabilities
19mAssociated Effects: Flexible Abstractions for Effectful Programming
55mRows and Capabilities as Modal Effects