Higher-order fork, modally
summary
Proposes a small Met extension that types a higher-order fork without effect variables by adding order-sensitive effect contexts and a notion of higher-order effects (high-order effect must be first in the context). Implements the idea in the Met-style modal effect types and shows a scheduled-queue example and a fork type that stores effectful functions, so the example runs, but the system currently has no proof of safety and remains work in progress.
AI-written summary · about
chapters (9)
- 0:00Higher-order fork problem
- 1:49Multi-shot continuations limits
- 3:15Effect typing approaches issues
- 5:45Model effect types framework
- 8:18Existing solutions problems
- 10:05Order-sensitive effect contexts
- 12:17Formal rules for higher-order effects
- 13:23Current work and future extensions
- 14:47Question and answer session
related talks
01h 06mThe Evolution of Effects
14mFundamentalist Functional Programming
50mFunctional Programming with Effects
43mFunctional Programming with Effects
25mHandling Higher-Order Effectful Operations with Judgemental Monadic Laws
54mRevisiting the Evolution of Effects (Invited Talk)
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
14mModal Effect Types