Maps in Functional Programming
Maps are ubiquitous data structures in programming. There are two maps: total maps, which have a “default” element to be returned when the key doesn’t exist; and partial maps, which returns an option to indicate success or failure1. Apparently, the latter is based on the former one.
Total Maps
There is a very unique and interesting way to define a total map, that is, using (higher-order) functions.
Definition total_map (A : Type) := string -> A.
Definition t_empty {A : Type} (v : A) : total_map A :=
(fun _ => v).
Definition t_update {A : Type} (m : total_map A)
(x : string) (v : A) :=
fun x' => if String.eqb x x' then v else m x'.
A map is a function string -> A. The function t_update takes a key-value pair and map, then returns a new function. This novelty here works because what we are talking about is a total map, which implies we don’t need to have a “delete” operation - To delete a key, we can just update the key to return the default value.
Here’s a few notations for (total) maps:
Notation "'_' '!->' v" := (t_empty v)
(at level 100, right associativity).
Notation "x '!->' v ';' m" := (t_update m x v)
(at level 100, v at next level, right associativity).
(* A map with 2 keys mapping to true: "bar" and "foo". *)
Definition examplemap' :=
( "bar" !-> true;
"foo" !-> true;
_ !-> false
).
With the help of notations, the use of maps seems to be really declarative. Some properties of map follows:
Property 1: If we update the map at key $x$ with value $v$, then we look up $x$, we will get $v$.
(* Exercise: t_update_eq *)
Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
(x !-> v ; m) x = v.
Proof.
intros A m x v.
unfold t_update. rewrite String.eqb_refl. reflexivity.
Qed.
Property 2: If we update a map at key $x_1$ and then look up a different key $x_2$, we get the same result before updating.
(* Exercise: t_update_neq *)
Theorem t_update_neq : forall (A : Type) (m : total_map A) x1 x2 v,
x1 <> x2 ->
(x1 !-> v ; m) x2 = m x2.
Proof.
intros A m x1 x2 v H.
unfold t_update.
destruct (String.eqb_spec x1 x2).
- unfold not in H. apply H in e. exfalso. apply e.
- reflexivity.
Qed.
Property 3: Update a map two times at the same key $x$ is equal to only perform the last update.
Notice that to reason about equality relation of two functions, we need the functional extensionality rule2.We say two functions are equal if on every possible input, both give same outputs. In other words, we don’t care about the internal structure of a function.
(* Exercise: t_update_shadow *)
Axiom functional_extensionality : forall {X Y: Type}
{f g : X -> Y},
(forall (x:X), f x = g x) -> f = g.
Lemma t_update_shadow : forall (A : Type) (m : total_map A) x v1 v2,
(x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).
Proof.
intros.
apply functional_extensionality. intros x'.
unfold t_update.
destruct (String.eqb_spec x x').
- trivial.
- trivial.
Qed.
Property 4: the operation that update a map m at x to assign the value as it already in m will not modify the map
Theorem t_update_same : forall (A : Type) (m : total_map A) x, (x !-> m x ; m) = m.
Proof.
intros.
unfold t_update.
apply functional_extensionality. intros x'.
destruct (String.eqb_spec x x').
- rewrite e. reflexivity.
- trivial.
Qed.
Property 5: if we update a map at two distinct keys, the order doesn’t matter.
Theorem t_update_permute : forall (A : Type) (m : total_map A)
v1 v2 x1 x2,
x2 <> x1 ->
(x1 !-> v1 ; x2 !-> v2 ; m)
=
(x2 !-> v2 ; x1 !-> v1 ; m).
Proof.
intros.
apply functional_extensionality. intros x.
unfold t_update.
destruct (String.eqb_spec x1 x) as [H0 | H0].
- destruct (String.eqb_spec x2 x) as [H1 | H2].
+ rewrite <- H0 in H1. unfold not in H. apply H in H1. contradiction.
+ reflexivity.
- destruct (String.eqb_spec x2 x) as [H1 | H2].
+ reflexivity.
+ reflexivity.
Qed.
Partial Map
We know that partial maps are built on the foundation of total maps. So basically they share same properties. But partial maps are more safe in practice.
Definition partial_map (A : Type) := total_map (option A).
Definition empty {A : Type} : partial_map A :=
t_empty None.
Definition update {A : Type} (m : partial_map A)
(x : string) (v : A) :=
(x !-> Some v ; m).
(** We introduce a similar notation for partial maps: *)
Notation "x '|->' v ';' m" := (update m x v)
(at level 100, v at next level, right associativity).
(** We can also hide the last case when it is empty. *)
Notation "x '|->' v" := (update empty x v)
(at level 100).
Definition examplepmap :=
("Church" |-> true ; "Turing" |-> false).