Type-driven Development with Idris

480 pages

Published March 31, 2017 by Manning Publications.


View on OpenLibrary

4 stars (1 review)

2 editions

A unique and thoughtful view of development

4 stars

This book got me interested in what expressive types can do for software development, maintenance, etc. While I never built anything real with Idris, I did love the programming approach versus that of Coq; I was able to express some type declarations that not only enforced a semantic correctness property, but also a worst-case runtime for the implementation.

I hope to see languages like Idris become more real-world useful, and more popular languages improve the expressiveness of their type systems.