Signature restriction for polymorphic algebraic effects
summary
Proposes signature restriction on effect interfaces: require each bound type variable to occur only strictly positively in argument positions and only positively in return positions. Proves that this simple polarity check is sufficient to restore type safety for algebraic effects under unrestricted let-polymorphism, gives a proof of soundness for a core type system, and supplies a separate type-and-effect system that lets signature-compliant effects be used polymorphically while non‑compliant effects remain monomorphic. Includes a tiny ML‑like implementation (effects assumed compliant).
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:29Title
- 1:30Example
- 3:18Problem
- 4:06Existing approaches
- 6:49New approach
- 7:16Summary
- 8:40Effect system
- 9:45Signature restriction overview
- 12:55Future work
- 13:40Conclusion
related talks
15mHandling Bidirectional Control Flow
15mQualified Types with Boolean Algebras
31mRethinking the Value Restriction
14mAdequacy for Algebraic Effects Revisited
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
22mType-Safe Code Generation With Algebraic Effects and Handlers
21mPolymorphic Type Inference for Dynamic Languages
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...