Idris for (im)practical Scala programmers
summary
Claims that Idris-style value-dependent types can be approximated in Scala by encoding: implicit search, phantom types, and type-level encodings of naturals and fin. Demonstrations recreate length-indexed vectors, fin-to-N conversions and format-string-style dependent functions using implicits and macros. The tools actually used are lambda-cube reasoning, pure-type-system ideas, Scala implicit resolution and macros. It works for compile-time-constant indices and format literals but breaks when values are truly runtime (loss of singleton/type preservation).
AI-written summary · about
chapters (8)
- 0:00Start
- 3:41Relating abstractions
- 10:20System F examples
- 13:37System Fw - examples
- 17:10Idris vs Scala
- 33:20Questions?
- 36:35type - Scala examples
- 38:07Scala vs Idris
related talks
40mScala vs Idris: Dependent types, now and in the future
48mA gentle introduction to type level programming in Scala
44mType level Computations in Scala
10mValue Your Types!
42mLet the Compiler Help You: How to Make the Most of Scala's Type System
50mThere's a prolog in your scala
49mThe Trouble With Types
30mConstraint Typing with Boolean Algebra