Chapter 10. Views: extending pattern matching

This chapter covers

  • Defining views, which describe alternative forms of pattern matching
  • Introducing the with construct for working with views
  • Describing efficient traversals of data structures
  • Hiding the representation of data behind views

In type-driven development, our approach to implementing functions is to write a type, define the structure of the function by case splits on its arguments, and refine the function by filling in holes. In the define step in particular, we use the structure of the input types to drive the structure of the function as a whole.

As you learned in chapter 3, when you case-split on a variable, the patterns arise from the variable’s type. Specifically, the patterns ...

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.