GADTs in Dotty
summary
Dotty implements GADTs that actually refine types on pattern match, preventing runtime casts: an expr evaluator returns the precise type after matching, length-indexed vectors enforce equal lengths for zip, and an EQ GADT proves type equalities. The compiler infers type constraints by upcasting scrutiny and patterns, rejecting impossible branches and handling unions, final types and variance. Dotty uniquely supports covariant GADTs and integrates with match types, fixing Scala 2 and Haskell limitations and making these checks compile-time reliable.
AI-written summary · about
chapters (6)
- 0:00Start
- 6:04List with type-level length
- 13:40Interesting covariant GADT: SUB
- 14:33Constraints from normal classes
- 23:12Back to invariance
- 24:52And a final detail
