Scala vs Idris: Dependent types, now and in the future
summary
A head-to-head of concrete engineering: Idris demonstrates full dependent types, builds sized vectors and an effects DSL that type-checks, compiles and runs, and statically rejects a forgotten file close (the resource-protocol example actually fails to type-check). Scala plus shapeless encodes the same patterns — sized lists, vconcat checks — but requires many explicit annotations, relies on implicits for proofs, and hit type-inference limits after about a week and a half of porting the effects DSL. Claims: Idris is practical for correctness; Scala can fake it but with heavy ergonomic cost.
AI-written summary · about
chapters (11)
- 0:00Introduction to computer errors
- 1:37The Mars climate orbiter crash
- 2:54Introduction to dependent types
- 5:19Idris language examples
- 10:09Computing with types
- 12:39Questions and answers
- 14:49Dependent types in Scala
- 21:19Translating Idris to Scala
- 27:51Resource usage protocols
- 31:49Challenges in Scala effects
- 37:20Conclusion
