From DOT to Dotty

This talk presents DOT, a calculus for expressing nested, parameterized modules with abstractable module types, and examines its type system and implications for language design. It also describes how Dotty implements DOT’s constructs and how those lessons inform Scala’s evolution.

Syllabus

Intro
Background
One Step Back
Why Do Foundations Matter?
Why Not Pick Existing Foundations?
Our Aim
Dependent Types in Code
Foundations: DOT
DOT Types
DOT Syntax in Greek
Definition Type Assignment
Subtyping
Expressiveness
Meta Theory
Programmer Definable Theorems
Bad Bounds
Dealing with it
For Details
Consequences for Language Design
Things To Avoid
What Are Implicit Function Types?
Contextual
Implicit Parameters
Example: Transaction Handling
Can We Do Better?
Towards A Solution
Two Rules for Typing
Revised Example (2)
Efficiency
The Builder Pattem
Scala Implementation
Claim
Summary