Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
summary
Presents a core calculus for higher-order effectful operations with higher-kinded impredicative polymorphism and optional recursion, where handlers live in lawless raw monads while computation typing enforces judgemental monadic laws. Gives a logical-framework presentation and realizability denotational models, and proves closed-term canonicity plus parametricity for the recursion-free fragment using synthetic Tait computability and a novel ⊤⊤-lifting. Shows scoped (deep) handlers reinstall automatically and argues that treating binds/monads judgementally simplifies equations and handler semantics.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:05Traditional compiler effects problems
- 3:32Code versioning without duplication
- 6:24Algebraic effects and handlers
- 7:27Handler handlers and higher-order effects
- 8:50Deep handlers and continuation reinstallation
- 10:36Limitations of quick handler approaches
- 12:42Scoped operations introduction
- 15:33Generic vs scoped operations differences
- 17:40Scoped operations with monadic bind
- 20:52Monadic interpretation of scoped handlers
- 21:55Categorical framework and logical relations
- 23:17System F omega with handlers
- 24:18Key takeaways
- 24:40Q&A
related talks
50mFunctional Programming with Effects
27mA General Fine-Grained Reduction Theory for Effect Handlers
43mFunctional Programming with Effects
28mA Series of Unfortunate Effects
01h 17mSmart Handlers: Handling the selection monad
14mFundamentalist Functional Programming
01h 06mThe Evolution of Effects
36mGoing Higher