Idris: Programming with Dependent Types

on YouTube ↗56m

" summary

Idris claims to bring full dependent types to practical programming with an optimising compiler and FFI, plus totality checker and tactic-based theorem proving. Demos build real artifacts: length-indexed vectors where append and zipWith are derived by the type checker, decidable-equality proofs and a verified run-length encoder, an effects library hooking IO, random and SDL into a small Space Invaders–style demo that compiles and runs. Installation uses cabal install Idris and examples live on GitHub.

AI-written summary · about

" chapters (5)

1. 0:00Start
2. 0:43Null Pointer Exceptions
3. 6:11Type Systems
4. 7:07Dependent Types
5. 8:38Natural Numbers

" related talks

• 58mThe Next Great Functional Programming LanguageJohn A De Goes · LambdaConf 2015
• 01h 46mWrite Some IdrisBrian McKenna · LambdaConf 2015
• 11mWhat are Dependent TypesStephan Boyer · LambdaConf 2017
• 35mProof Theory Impressionism: Blurring the Curry-Howard LineDan Pittman · Strange Loop 2018
• 01h 03mKeynote: Why Functional Programming MattersJohn Hughes, Mary Sheeran · Lambda Days 2017
• 39mA Little Taste of Dependent TypesDavid Christiansen · Strange Loop 2018
• 01h 04mThe Leibniz Library and Applied Propositions as TypesAlexander Konovalov · LambdaConf 2018
• 56mThe Making of an IODaniel Spiewak · Scala.IO 2017