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.

8.1. Guaranteeing equivalence of data with equality types

8.1.1. Implementing exactLength, first attempt

8.1.2. Expressing equality of Nats as a type

8.1.3. Testing for equality of Nats

8.1.4. Functions as proofs: manipulating equalities

8.1.5. Implementing exactLength, second attempt

8.1.6. Equality in general: the = type

8.2. Equality in practice: types and reasoning

8.2.1. Reversing a vector

8.2.2. Type checking and evaluation

8.2.3. The rewrite construct: rewriting a type using equality

8.2.4. Delegating proofs and rewriting to holes

8.2.5. Appending vectors, revisited

8.3. The empty type and decidability

8.3.1. Void: a type with no values

8.3.2. Decidability: checking properties with precision

8.3.3. DecEq: an interface for decidable equality

8.4. Summary