Type-Driven Development with Idris

Chapter 9. Predicates: expressing assumptions and contracts in types

This chapter covers

• Describing and checking membership of a vector using a predicate
• Using predicates to describe contracts for function inputs and outputs
• Reasoning about system state in types

Dependent types like EqNat and =, which you saw in the previous chapter, are used entirely for describing relationships between data. These types are often referred to as predicates, which are data types that exist entirely to describe a property of some data. If you can construct a value for a predicate, then you know the property described by that predicate must be true.

In this chapter, you’ll see how to express more-complex relationships between data using predicates. By expressing ...