Type-Driven Development with Idris

Acknowledgments

Many people have helped in the writing of this book, and it wouldn’t exist without them. In particular, I thank Dan Maharry, who encouraged me to reveal the ideas of type-driven development much more clearly. The mantra of “type, define, refine,” which appears throughout the book, was Dan’s suggestion. I also owe many thanks to Andrew Gibson, who has meticulously worked through all the examples and exercises throughout the book, making sure they work, checking that the exercises are solvable, and suggesting many improvements to the text and explanations. Overall, I’d like to thank the team at Manning Publications for helping to make this book a reality.

The design of Idris owes much to several decades of research into type theory, ...