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 arise from the data constructors that can be used to build values of that type. For example, if you case-split on an items variable of type List elem, the following patterns will arise:

  • []—Represents the empty list
  • (x :: xs)—Represents a non-empty list with x as the first element and xs as the list of the remaining elements

Pattern matching, therefore, deconstructs variables into their components. Often, though, you’ll want to deconstruct variables in different ways. For example, you might want to deconstruct an input list into one of the following forms:

  • A list of all but the last element, and then the last element
  • Two sublists—the first half and the second half of the input

10.1. Defining and using views

10.1.1. Matching the last item in a list

10.1.2. Building views: covering functions

10.1.3. with blocks: syntax for extended pattern matching

10.1.4. Example: reversing a list using a view

10.1.5. Example: merge sort

10.2. Recursive views: termination and efficiency

10.2.1. “Snoc” lists: traversing a list in reverse

10.2.2. Recursive views and the with construct

10.2.3. Traversing multiple arguments: nested with blocks

10.2.4. More traversals: Data.List.Views

10.3. Data abstraction: hiding the structure of data using views

10.3.1. Digression: modules in Idris

10.3.2. The data store, revisited

10.3.3. Traversing the store’s contents with a view

10.4. Summary