DOT: Scala Types from Theory to Practice
summary
Presents Dependent Object Types as the core calculus used in Dotty, proves soundness by modeling path‑dependent type members, unions/intersections and a store semantics, and fixes unsound “bad bounds” that cause lattice collapse and runtime cast failures in Scala. Key techniques: differentiate concrete vs abstract variables at runtime, require computable prefixes for selections, and check recursive bounds syntactically in the calculus. Result: Dotty’s type checker is simpler and catches some errors Scala’s does not.
AI-written summary · about
chapters (7)
- 0:00Start
- 4:23Types in Scala
- 8:10Foundations
- 26:48(My) (DOT) Journey
- 27:35Retrospective: What matters for soundness
- 29:48A between Scala & DOT
- 35:36Higher-Kinded Types?
related talks
49mFrom DOT to Dotty
37mThe DOT Calculus: An Introduction for Scala Programmers
30mDotty and types: the story so far
01h 00mState of Dotty
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
01h 39mHands-on Dotty
14mιDOT: A DOT Calculus with Object Initialization
19mDeriving Dependently-Typed OOP from First Principles