Idris For (Im)practical Scala Programmers
summary
Scala can encode many dependent‑type patterns but only for compile‑time known values: it uses singleton types, path‑dependent types and recursive implicit search plus macros/transparent functions to build length‑indexed vectors, conversions between literal integers and type‑level naturals, and precise printf format types. The technique preserves exact types via dependent methods and implicit evidence and it works for constants and compile‑time witnesses, but it breaks when singleton structure is lost so runtime lengths, general filter results and arbitrary variable formats are not dependently typed.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:51Type system theory overview
- 10:31Lambda Cube and expressiveness
- 20:04Dependent typing in Scala
- 33:45Practical limitations in Scala
- 43:43Q&A
related talks
49mAcademese to English: Scala's Type System, Dependent Types and What It Means To You
45mTypelevel Programming 101: The Subspace of Scala
24mLet the Scala compiler work for you
48mAcademese to English: A Practical Tour of Scala’s Type System
49mType level Programming in Scala
26mAn Independent History of Implicit Language Application
45mHow to be polymorphic in Scala
30mDotty and types: the story so far