Type level Programming in Scala
summary
Scala 3 uses match types plus literal, singleton and refinement types to compute precise argument tuples for examples like a compile-time printf parser, a strongly-typed regex extractor and typed HTTP routes; a compiler prototype adds type-level arithmetic normalization (ordering and grouping but no automatic distribution) so non-constant sizes compare (e.g. xy == yx) and sized-vector operations and map typechecks; normalization is lazy, implemented in the compiler, and termination checks are currently stack-based only.
AI-written summary · about
chapters (14)
- 0:00Introduction to precise types
- 1:32The necessity of type systems
- 3:33Literal and dependent types
- 5:57Type equality and refinements
- 9:21Compile-time operations
- 10:34Match types and printf example
- 13:21Implementing complex match types
- 17:53Type-safe HTTP routing
- 22:22Implementing the router
- 28:04Type-level arithmetic
- 32:52Normalization and reasoning
- 37:47Type-safe algorithms
- 40:51Challenges and future ideas
- 45:50Q&A session
related talks
45mTypelevel Programming 101: The Subspace of Scala
43mEffective Match Types
32mUnderstanding the Type System of Scala 3
38mThinking in Scala 3 Types
42mPolymorphic Function Types in Scala 3
19mLogically Qualified Types for Scala 3
24mLet the Scala compiler work for you
40mPolymorphic Function Types in Scala 3