Chapter 9. Predicates: expressing assumptions and contracts 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 relationships between data in types, you can be explicit about the assumptions you’re making about the inputs to a function, and have those assumptions checked by the type checker when those functions are called. You can even think of these assumptions as expressing compile time contracts that other arguments must satisfy before anything can call the function.

In practice, you’ll often write functions that make assumptions about the form of some other data, having (hopefully!) checked those assumptions beforehand. Here are a few examples:

9.1. Membership tests: the Elem predicate

9.1.1. Removing an element from a Vect

9.1.2. The Elem type: guaranteeing a value is in a vector

9.1.3. Removing an element from a Vect: types as contracts

9.1.4. auto-implicit arguments: automatically constructing proofs

9.1.5. Decidable predicates: deciding membership of a vector

9.2. Expressing program state in types: a guessing game

9.2.1. Representing the game’s state

9.2.2. A top-level game function

9.2.3. A predicate for validating user input: ValidInput

9.2.4. Processing a guess

9.2.5. Deciding input validity: checking ValidInput

9.2.6. Completing the top-level game implementation

9.3. Summary