Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
summary
Introduces the cDOT calculus as a formal foundation that encodes subtyping information uncovered by pattern matching, builds on pDOT and DOT-style structural types, and formalizes subtyping reconstruction via subtyping assumptions plus internalized inversion lemmas. Proves a type-preserving translation of λ2,Gµ into cDOT, showing GADT-style reasoning is subsumed, and reports a prototype Scala implementation modeling the approach; the calculus scales to generic inheritance, variance, F-bounds, and first-class recursive modules.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:18Objects with Pattern Matching
- 8:55Towards formal reasoning: revisiting eval
- 10:29Formal foundations: CDOT
- 12:23CDOT: representing classes
- 15:07CDOT: typing eval
- 17:16CDOT type forms
- 19:05Tagged objects
- 20:23Subtyping reconstruction, formally
- 20:50Subtyping assumptions: reflecting type member bounds in subtyping
- 22:19Subtyping inversion
- 23:46Reconnecting with existing theory
- 24:08Separate context for assumptions
related talks
49mFrom DOT to Dotty
42mDOT: Scala Types from Theory to Practice
37mThe DOT Calculus: An Introduction for Scala Programmers
14mιDOT: A DOT Calculus with Object Initialization
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
18mThe Essence of Generalized Algebraic Data Types
14mScala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
23mType-Level Programming with Match Types