This brief chapter defines two kinds of maps: total maps, which include a default element to be returned when a key being looked up does not exist, and partial maps, which return an option to indicate success or failure. We'll use maps in upcoming chapters to verify other data structures.

Total Maps

The Lists chapter in Volume 1 previously implemented maps with lists of key-value pairs. Here, we instead use functions to implement maps. Functions enable an extensional treatment of maps: two maps will be equal if they take the keys to the same values. We won't have to worry about issues that arise with lists, such as duplicate keys, or order of pairs in the list, etc. Proofs that use maps will therefore be simpler. Intuitively, a total map over a type A is just a function that can be used to look up keys, yielding As. For simplicity, the keys in our maps will be natural numbers.

The function t_empty yields an empty total map, given a default element; this map always returns the default element when applied to any id.

More interesting is the update function, which (as before) takes a map m, a key x, and a value v and returns a new map that takes x to v and takes every other key to whatever m does.

This definition is a nice example of higher-order programming. The t_update function takes a function m and yields a new function fun x' ⇒ ... that behaves like the desired map. For example, we can build a map taking ids to bools, where Id 3 is mapped to true and every other key is mapped to false, like this:

This completes the definition of total maps. Note that we don't need to define a find operation because it is just function application!

To use maps in later chapters, we'll need several fundamental facts about how they behave. Even if you don't work the following exercises, make sure you thoroughly understand the statements of the lemmas! (Some of the proofs require the functional_extensionality axiom, which is discussed in the Logic chapter.)

Exercise: 1 star, standard (t_apply_empty)

The empty map returns its default element for all keys:

Exercise: 1 star, standard (t_update_eq)

If we update a map m at a key x with a new value v and then look up x in the map resulting from the update, we get back v:

Exercise: 1 star, standard (t_update_neq)

If we update a map m at a key x₁ and then look up a different key x₂ in the resulting map, we get the same result that m would have given:

Exercise: 1 star, standard (t_update_shadow)

If we update a map m at a key x with a value v₁ and then update again with the same key x and another value v₂, the resulting map behaves the same (gives the same result when applied to any key) as the simpler map obtained by performing just the second update on m:

Exercise: 1 star, standard (t_update_same)

If we update a map to assign key x the same value as it already has in m, then the result is equal to m:

Exercise: 1 star, standard (t_update_permute)

If we update a map m at two distinct keys, it doesn't matter in which order we do the updates.

Partial Maps

A partial map with elements of type A is simply a total map with elements of type option A and default element None.

We can easily lift all of the basic lemmas about total maps to partial maps.