Type-Driven Development in Idris — Edwin Brady

Archive guide

Edwin Brady, creator of Idris, introduces type-driven development in a dependently typed language. He shows types being written first and programs derived with interactive editing, then extends beyond simple examples to programs that interact with users and networks.