Part 3. Idris and the real world
In part 2, you gained experience in developing programs interactively, guided by types, and you learned about all of the core features of Idris. Now, it’s time to apply what you’ve learned to some more practical examples.
First, in chapter 11, you’ll learn about writing programs that deal with potentially infinite structures such as streams. You’ve learned about the importance of writing total functions, but in chapter 11 you’ll see that totality is about more than termination. A function is also total if it produces some portion of a potentially infinite result, which means you can write interactive systems such as servers and read-eval-print loops that run forever, but which are nevertheless total.
Get Type-Driven Development with Idris now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
