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 then, in chapter 4, you’ll learn to define your own data types and build larger programs around them. Chapter 5 shows how you can write programs that interact with the outside world, using types to separate evaluation from execution. Later chapters introduce more-advanced concepts in type-driven development, including type-level computation in chapter 6, working with constrained generic types in chapter 7, describing and proving properties of programs in chapters 8 and 9, and defining alternative traversals of data structures using views in chapter 10.
By the end of part 2, you’ll have learned about all of the core features of Idris.