From DOT to Dotty
summary
A formal, minimal calculus called DOT (Dependent Object Types) serves as the blueprint for Scala’s next core and exposes the real tradeoffs: proving type soundness takes years of work and forces language changes (no unchecked type selections from lazy vals, restrictions on null and initialization). A new prototype Dotty compiler implements DOT, already encoding generics as type members and spotting 2,641 implicit-context sites; a proposed implicit function types feature replaces repeated implicit parameters, is optimizable to zero runtime overhead, and supports contextual DSLs like builders and transactional scopes.
AI-written summary · about
chapters (32)
- 0:00Intro
- 0:57Background
- 2:13One Step Back
- 4:59Why Do Foundations Matter?
- 5:33Why Not Pick Existing Foundations?
- 6:37Our Aim
- 8:23Dependent Types in Code
- 10:38Foundations: DOT
- 11:11DOT Types
- 15:41DOT Syntax in Greek
- 19:22Definition Type Assignment
- 20:15Expressiveness
- 21:31Meta Theory
- 22:44Programmer Definable Theorems
- 23:26Bad Bounds
- 25:10Dealing with it
- 25:58For Details
- 26:13Consequences for Language Design
- 26:43Things To Avoid
- 31:08What Are Implicit Function Types?
- 31:22Contextual
- 32:03Implicit Parameters
- 32:58Example: Transaction Handling
- 36:04Can We Do Better?
- 37:13Towards A Solution
- 38:50Two Rules for Typing
- 40:50Revised Example (2)
- 42:40Efficiency
- 43:41The Builder Pattem
- 44:54Scala Implementation
- 46:25Claim
- 47:12Summary
