Part 2. Core Idris
Now that you have some experience writing programs in Idris, it’s time to start your exploration of type-driven development in depth. In this part, you’ll learn about the core features of Idris and gain some experience in the process of type-driven development. Rather than showing you complete programs right from the start, I’ll show you how to build programs interactively, via a process of type, define, refine:
- Type— Write a type for a function.
- Define— Create an initial definition for the function, possibly containing holes.
- Refine— Complete the definition by filling in holes, possibly modifying the type as your understanding of the problem develops.
In chapter 3, you’ll learn the basics of interactive development; and ...
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.
