A Type-and-Effect System for Object Initialization
summary
Type-and-effect design enforces a concretely checkable initialization discipline: cold, warm, hot types plus potentials and effects track field accesses, method calls and promotions so the checker rejects uses of uninitialized fields and enforces perfect monotonicity. Implementation is a Scala 3 compiler phase that requires zero core-type changes, emits stacktrace-style diagnostics, and runs on ~500k LOC with about 0.6 warnings/KLOC. Examples include rejected virtual-call and aliasing patterns that would yield nulls at runtime.
AI-written summary · about
chapters (22)
- 0:00Intro
- 0:14A 50-year old problem
- 1:59Can we disallow usage of this before initialization?
- 2:54Challenge 1: virtual method calls
- 3:39Challenge 2: aliasing
- 4:35Local reasoning about initialization
- 5:40Three pillars of local reasoning
- 5:55Weak Monotonicity
- 6:08Stackability
- 6:28Scopability
- 7:05Abstractions: cold, warm and hot
- 9:16Perfect Monotonicity
- 10:07Drawbacks of type-based approach
- 10:41Type-and-effect systems
- 11:12Example - field access effect
- 11:36Example - method call effects
- 12:04Example - potentials
- 12:59Example - escape
- 13:55Potentials and effects
- 14:49Implementation
- 15:09Experiment
- 15:19Conclusion
related talks
51mEffects: to be or not to be?
22mType-Safe Code Generation With Algebraic Effects and Handlers
19mIll-Typed Programs Don't Evaluate
27mLimiting side-effects of applications at compile-time
12mTowards Dependently-Typed Control Effects (Extended Abstract)
30mDotty and types: the story so far
42mDOT: Scala Types from Theory to Practice
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers