Value Your Types!
summary
Types encode concrete properties now: dependent types express “non‑negative” or “length‑N” constraints, shown with Idris vectors where the type carries the list length. Implementations include pairwise add that returns a vector of the same length and append whose result type is n+m, and the compiler can enforce Idris enforces totality so missing cases or nontermination are flagged. Caveat: allowing arbitrary value computation in types makes equivalence undecidable, and a real socket library was found broken when attempted for a demo.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:16What are dependent types
- 1:50The history of dependent types
- 3:27Address
- 4:58Pair
- 6:38Totality
- 7:01Practical Examples
- 7:49A Brief Aside
- 9:00Undecidability
related talks
49mIdris for (im)practical Scala programmers
40mScala vs Idris: Dependent types, now and in the future
35mGADTs and You; Writing Safer Code Using GADTs
45mDepending on Types
44mA Deep Dive Into Advanced Typescript: A Live Coding Expedition
38mType Systems - The Good, Bad and Ugly
47mCommunicating in Types
11mAlgebraic Data Types