A gentle introduction to type level programming in Scala
summary
Shows concrete, mechanical rules to turn value‑level Scala into type‑level code and demonstrates them by implementing boolean types, Peano numbers, and a sized IntList so that adding lists of different lengths fails at compile time instead of throwing exceptions. Uses plain Scala for translation, relies only on shapeless’s typecheck macro for negative tests, exercises implicitly‑based compile‑time assertions, and runs examples that compile successfully; notes readability pain and rising compile times (examples can push compilation to around fifteen seconds).
AI-written summary · about
chapters (6)
- 0:00Start
- 28:24STARTING AT THE VALUE LEVEL
- 31:36THE TRANSLATION #1
- 34:52THE TRANSLATION #2
- 35:29THE TRANSLATION #3
- 38:12FINAL CODE
related talks
44mType level Computations in Scala
42mLet the Compiler Help You: How to Make the Most of Scala's Type System
50mThere's a prolog in your scala
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell
48mTypelevel Scala: What does it mean ?
28mSecrets of the Scala Type System
49mThe Trouble With Types
44mTelling the Truth with Types