The DOT Calculus: An Introduction for Scala Programmers
summary
Small core calculus formalizes the Scala 3-ish type system and claims type soundness with fully mechanized proofs verifying that well-typed programs do not get typing errors. It models path-dependent types, dependent function types, intersections as symmetric sets, and encodes classes and polymorphism by objects and type members (encodes classes via abstract type members). It omits inheritance and some Scala features, carries subtyping proofs as runtime values, and leaves decidable type checking unresolved.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:33What is DOT?
- 1:02Scala Examples
- 9:20Core DOT Concepts
- 15:01DOT Syntax Grammar
- 24:38Type System Mechanics
- 36:16Conclusion
related talks
49mFrom DOT to Dotty
42mDOT: Scala Types from Theory to Practice
14mιDOT: A DOT Calculus with Object Initialization
49mAcademese to English: Scala's Type System, Dependent Types and What It Means To You
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
01h 00mState of Dotty
38mThinking in Scala 3 Types
30mDotty and types: the story so far