Skip to content
0:00 / 0:00

#dot-calculus#dotty#scala-3

SPLASH 2016 Keynote: From DOT to Dotty -- Foundations and Types for Objects As Modules

SPLASH2016

70 subscribers • 2 videos on Hallway

YouTube
  • Recommended by 2 people: 2 in engineering communities.
  • Presented by Martin Odersky

Advanced. Deep dive for people who know the field.

646 views9 years ago2 recommendations

Programming languagesComputer scienceScalaLanguage design and type systemsCompilers and interpreters

Martin Odersky presents the DOT calculus and how it serves as the foundation for the Dotty compiler and Scala.

The utility of objects derives to a large degree form the fact that objects are natural modules, that is, building blocks from which larger modules are defined. Static type systems are essential for fine grained control what information is exposed in a module, and, conversely, what one is free to change inside a module. A good module or object system should follow three principles: Everything can be nested in a module. Everything can be parameterized with a module. Module types are interfaces, which can be abstracted. In this talk I present DOT, a particularly simple calculus that can express systems following these principles. DOT has been developed as the foundation of the next version of Scala. I will also report on dotty, a new Scala compiler that implements the constructs of DOT in its core data structures and that synthesizes object oriented and functional programming concepts in several interesting new patterns.

Why it's here

2 people recommend this

What people say. Recommended for its deep dive into the soundness of Scala's type system and the theoretical foundations of Dotty.

u/oelangin r/scala • Recommends

SPLASH 2016 Keynote: From DOT to Dotty -- Foundations and Types for Objects As Modules

u/mdedetrichin r/scala • Recommends

On “"Java and Scala's Type Systems are Unsound"”

…that the two approaches are actually very different. Also trying to prove correctness in languages which are practical to use are almost always feasibly impossible. Dotty for example doesn't try to prove correctness in its entirety, it can only prove the instantiated values are valid, and Martin goes into detail as to why this is so in this talk link to this video…