Type-Driven Development with Idris

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 ...