Type-driven Development with Idris

SummaryType-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed to support type-driven development.Purchase of the print book includes a free eBook in PDF, Kindle, and ePub formats from Manning Publications.About the TechnologyStop fighting type errors! Type-driven development is an approach to coding that embraces types as the foundation of your code - essentially as built-in documentation your compiler can use to check data relationships and other assumptions. With this approach, you can define specifications early in development and write code that's easy to maintain, test, and extend. Idris is a Haskell-like language with first-class, dependent types that's perfect for learning type-driven programming techniques you can apply in any codebase.About the BookType-Driven Development with Idris teaches you how to improve the performance and accuracy of your code by taking advantage of a state-of-the-art type system. In this book, you'll learn type-driven development of real-world software, as well as how to handle side effects, interaction, state, and concurrency. By the end, you'll be able to develop robust and verified software in Idris and apply type-driven development methods to other languages.What's InsideUnderstanding dependent typesTypes as first-class language constructsTypes as a guide to program constructionExpressing relationships between dataAbout the ReaderWritten for programmers with knowledge of functional programming concepts.About the AuthorEdwin Brady leads the design and implementation of the Idris language.Table of ContentsPART 1 - INTRODUCTIONOverviewGetting started with IdrisPART 2 - CORE IDRISInteractive development with typesUser-defined data typesInteractive programs: input and output processingProgramming with first-class typesInterfaces: using constrained generic typesEquality: expressing relationships between dataPredicates: expressing assumptions and contracts in typesViews: extending pattern matchingPART 3 - IDRIS AND THE REAL WORLDStreams and processes: working with infinite dataWriting programs with stateState machines: verifying protocols in typesDependent state machines: handling feedback and errorsType-safe concurrent programming Types are often seen as a tool for checking errors, with the programmer writing a complete program first and using the type checker to detect errors. And while tests are used to show presence of errors, they can only find errors that you explicitly test for. In type-driven development, types become your tools for constructing programs and, used appropriately, can show the absence of errors. And you can express precise relationships between data, your assumptions are explicit and checkable, and you can precisely state and verify properties. Type-driven development lets users write extensible code, create simple specifications very early in development, and easily create mock implementation for testing. This book, written by the creator of Idris, teaches programmers how to improve the performance and accuracy of programs by taking advantage of a state-of-the-art type system Type-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed from the very beginning to support type-driven development. In this book, youll learn how to manipulate types just like any other construct (numbers, strings, lists, etc.). Youll see how to use type-driven development to build real-world software, as well as how to handle side-effects, state and concurrency, and interoperating with existing systems. By the end of this book, you will be able to develop robust and verified software in Idris and apply type-driven development methods to programming in other languages.

Type-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed to support type-driven development.