Book description
Type-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.
Table of contents
- Type-Driven Development with Idris
- Copyright
- Brief Table of Contents
- Table of Contents
- Preface
- Acknowledgments
- About this Book
- About the Author
- About the Cover Illustration
- Part 1. Introduction
- Chapter 1. Overview
- Chapter 2. Getting started with Idris
- Part 2. Core Idris
- Chapter 3. Interactive development with types
- Chapter 4. User-defined data types
- Chapter 5. Interactive programs: input and output processing
- Chapter 6. Programming with first-class types
- Chapter 7. Interfaces: using constrained generic types
- Chapter 8. Equality: expressing relationships between data
- Chapter 9. Predicates: expressing assumptions and contracts in types
- Chapter 10. Views: extending pattern matching
- Part 3. Idris and the real world
- Chapter 11. Streams and processes: working with infinite data
-
Chapter 12. Writing programs with state
- 12.1. Working with mutable state
- 12.2. A custom implementation of State
-
12.3. A complete program with state: working with records
- 12.3.1. Interactive programs with state: the arithmetic quiz revisited
- 12.3.2. Complex state: defining nested records
- 12.3.3. Updating record field values
- 12.3.4. Updating record fields by applying functions
- 12.3.5. Implementing the quiz
- 12.3.6. Running interactive and stateful programs: executing the quiz
- 12.4. Summary
- Chapter 13. State machines: verifying protocols in types
- Chapter 14. Dependent state machines: handling feedback and errors
-
Chapter 15. Type-safe concurrent programming
- 15.1. Primitives for concurrent programming in Idris
-
15.2. Defining a type for safe message passing
- 15.2.1. Describing message-passing processes in a type
- 15.2.2. Making processes total using Inf
- 15.2.3. Guaranteeing responses using a state machine and Inf
- 15.2.4. Generic message-passing processes
- 15.2.5. Defining a module for Process
- 15.2.6. Example 1: List processing
- 15.2.7. Example 2: A word-counting process
- 15.3. Summary
- Appendix A. Installing Idris and editor modes
- Appendix B. Interactive editing commands
- Appendix C. REPL commands
- Appendix D. Further reading
- Appendix E.
- Appendix F.
- Index
- List of Figures
- List of Tables
- List of Listings
Product information
- Title: Type-Driven Development with Idris
- Author(s):
- Release date: March 2017
- Publisher(s): Manning Publications
- ISBN: 9781617293023
You might also like
book
Elm in Action
Elm in Action teaches you the Elm language along with a new approach to coding frontend …
book
Head First Design Patterns, 2nd Edition
You know you don’t want to reinvent the wheel, so you look to design patterns—the lessons …
book
Functional Programming in Scala
Functional Programming in Scala is a serious tutorial for programmers looking to learn FP and apply …
book
Grokking Algorithms
Grokking Algorithms is a friendly take on this core computer science topic. In it, you'll learn …