Chapter 8. Equality: expressing relationships between data
This chapter covers
- Expressing properties of functions and data
- Checking and guaranteeing equalities between data
- Showing when cases are impossible with the empty type Void
You’ve now seen several ways in which first-class types increase the expressivity of the type system, and the precision of the types we give to functions. You’ve seen how to use increased precision in types (along with holes) to help write functions, and how to write functions to calculate types. Another way you can use first-class types to increase the precision of your types, and to increase confidence in functions behaving correctly, is to write types specifically to express properties of data and the relationships between data.
In this chapter, we’ll look at a simple property, using types to express guarantees that values are equal. You’ll also see how to express guarantees that values are not equal. Properties such as equality and inequality are sometimes required when you’re defining more-complex functions with dependent types, where the relationship between values might not be immediately obvious to Idris. For example, as you’ll see when we define reverse on vectors, the input and output vector lengths must be the same, so we’ll need to explain to the compiler why the length is preserved.
We’ll start by looking at a function we’ve already used, exactLength, and see in some detail how to build it from first principles.