Type-Driven Development in Idris

on YouTube ↗47m

" summary

Idris provides first‑class dependent types and interactive tools (REPL, case‑split, expression search) that drive development: the language types compute values (printf format strings), enforce invariants (vectors with length-indexed zipWith and a transposer that compiles and runs), model stateful APIs via the effects library (door protocol with jam handling), and yield a verified Hangman implementation plus a Space‑Invaders demo; code compiles to C/JavaScript (and a PHP backend) and the live examples run successfully, claiming practical “Pac‑Man complete” usability.

AI-written summary · about

" chapters (7)

1. 0:00Introduction to Idris
2. 4:05Type-driven development
3. 6:57Idris language features
4. 13:54Type-driven programming demos
5. 24:05Advanced vector manipulation
6. 30:48State machines and effects
7. 40:52Conclusion and resources

" related talks

• 41mType-driven Development of Communicating Systems in IdrisEdwin Brady · Lambda World 2016
• 41mPrograms and Proofs — Dependent Typing as a Way to Structure Your CodeGuillaume Andrieu · DevFest Toulouse 2023
• 40mQuantitative Types in Idris 2Edwin Brady · SPLASH 2020 REBASE
• 41mFun With CategoriesMarco Perone · Lambda World Cádiz 2019
• 19mColouring Flags with Dafny & IdrisJames Noble, Jan de Muijnck-Hughes · Dafny 2024
• 45mTDD, as in Type-Directed DevelopmentClement Delafargue · JavaDay Lviv 2015
• 20mInteractive Haskell Type Inference Exploration (Extended Abstract)Peter J. Stuckey, Tim Dwyer, Shuai Fu · TyDe 2021
• 51mFunctional Programming and Domain Driven Design - a match in Heaven!Marco Emrich · KanDDDinsky 2019