Idris: Practical Dependent Types with Practical Examples
summary
Idris compiles executable dependent‑type code and shows concrete outcomes: proved associativity of bitwise or using tactics and proof search, implemented typed binary literals and conversion, and embeds runnable examples as types. A small window manager (Idium window manager) actually runs, demonstrating practical compilation. A dependent cost monad expresses and checks factorial cost bound and prevents running beyond a finited bound (<7). Proof search, implicit arguments and Auto do much inference; some claims use explicit assertions (casts) and the implementation shows a few non‑total warnings.
AI-written summary · about
chapters (5)
- 0:00Start
- 3:51Iridium
- 5:10Proof of an Algebraic Law about a Data Type
- 13:46Expressiveness of Depend Types
- 19:29Proof Search
related talks
01h 20mA Practical Introduction to Haskell GADTs
49mType Theory Behind the Glasgow Haskell Compiler Internals (Part 2)
51mPragmatism, Puritanism and Functional Programming
01h 52mIsomorphic Reasoning: Counting with Types Part 3
38mPropositions as Types for Beginners in Haskell
02h 28mIsomorphic Reasoning: Counting with Types Part 2
01h 01mType Theory Behind the Glasgow Haskell Compiler Internals (Part 6)
01h 39mIsomorphic Reasoning: Counting with Types Part 1