In retrospect, it would have been useful to sketch the effect of list_map, list_fold_right, and list_fold_left. The goal of the present chapter is to draw these sketches.
Given two types V and W, a function f of type V -> W, and a list of elements of V, list_map homomorphically constructs a list of elements of W that are the result of applying f to each successive element of the given list. (N.B.: “homomorphic” means “structure-preserving”.) The following property captures this characterization for all the lists of length 0 to 3:
Property a_sketchy_characterization_of_list_map :
forall list_map : forall V W : Type, (V -> W) -> list V -> list W,
specification_of_list_map list_map ->
forall (V W : Type)
(f : V -> W),
( list_map V W f nil = nil)
/\
(forall v3 : V,
list_map V W f (v3 :: nil) = f v3 :: nil)
/\
(forall v2 v3 : V,
list_map V W f (v2 :: v3 :: nil) = f v2 :: f v3 :: nil)
/\
(forall v1 v2 v3 : V,
list_map V W f (v1 :: v2 :: v3 :: nil) = f v1 :: f v2 :: f v3 :: nil).
Prove Property a_sketchy_characterization_of_list_map.
Characterize the following computations:
V is nat, W is nat, and f is fun n : nat => n:
Check (a_sketchy_characterization_of_list_map
list_map
list_map_satisfies_the_specification_of_list_map
nat
nat
(fun n : nat => n)).
V is nat, W is nat, and f is fun n : nat => S n:
Check (a_sketchy_characterization_of_list_map
list_map
list_map_satisfies_the_specification_of_list_map
nat
nat
(fun n : nat => S n)).
for any given type V, W is V, and f is fun v : V => v:
Check (fun (V : Type) =>
a_sketchy_characterization_of_list_map
list_map
list_map_satisfies_the_specification_of_list_map
V
V
(fun v : V => v)).
for any given type V, W is list V, and f is fun v : V => v :: nil:
Check (fun (V : Type) =>
a_sketchy_characterization_of_list_map
list_map
list_map_satisfies_the_specification_of_list_map
V
(list V)
(fun v : V => v :: nil)).
for any given type V, W is V * V, and f is fun v : V => (v, v):
Check (fun (V : Type) =>
a_sketchy_characterization_of_list_map
list_map
list_map_satisfies_the_specification_of_list_map
V
(V * V)
(fun v : V => (v, v))).
Pablito: What are we supposed to do?
Bong-sun: I think we should first look at the result of running the Check command.
Halcyon (courteous): The *goals* window then reads:
a_sketchy_characterization_of_list_map list_map list_map_satisfies_the_specification_of_list_map nat nat
(fun n : nat => n)
: list_map nat nat (fun n : nat => n) nil = nil /\
(forall v3 : nat, list_map nat nat (fun n : nat => n) (v3 :: nil) = v3 :: nil) /\
(forall v2 v3 : nat, list_map nat nat (fun n : nat => n) (v2 :: v3 :: nil) = v2 :: v3 :: nil) /\
(forall v1 v2 v3 : nat, list_map nat nat (fun n : nat => n) (v1 :: v2 :: v3 :: nil) = v1 :: v2 :: v3 :: nil)
Pablito: Huh?
Bong-sun: Let me reformat the contents of this window for readability:
a_sketchy_characterization_of_list_map list_map list_map_satisfies_the_specification_of_list_map nat nat
(fun n : nat => n)
: list_map nat nat (fun n : nat => n) nil = nil
/\
(forall v3 : nat,
list_map nat nat (fun n : nat => n) (v3 :: nil) = v3 :: nil)
/\
(forall v2 v3 : nat,
list_map nat nat (fun n : nat => n) (v2 :: v3 :: nil) = v2 :: v3 :: nil)
/\
(forall v1 v2 v3 : nat,
list_map nat nat (fun n : nat => n) (v1 :: v2 :: v3 :: nil) = v1 :: v2 :: v3 :: nil)
Pablito: Ah, OK, the same formatting as the sketchy characterization of list_map. Thanks.
Anton: What was the point of this characterization again?
Alfrothul: The point was to sketch the effect of applying list_map to the empty list, to a singleton list, to a list of two elements, and to a list of three elements.
Bong-sun: So the point of the present characterization is also to sketch the effect of applying list_map to four lists of increasing length when the function that is mapped is the identity function over natural numbers.
Anton: OK. And that’s it?
Dana: On the surface of it yes, but Mimer keeps telling us that we should start – not stop – to think when we found a solution.
Anton (pragmatic): So what should we think about?
Dana: Déjà vu, for example. Have we see this solution before? Or something like it?
Anton: You mean have we already mapped the identity function over a list?
Dana: Yes.
Bong-sun: We have. In the midterm project. To implement list_copy as an instance of list_map.
Dana: Right. For lists of natural numbers.
Bong-sun: So, list_copy nat?
Dana: Yes.
Anton: You mean that this exercise is a sketchy revisitation of the midterm project?
Alfrothul: Looks like, Anton. Looks like.
The fourth wall: Would you guys like to look at Exercise 02.b?
Alfrothul (decisive): Let’s.
Dana: Thanks, Fourth Wall.
Pablito: Let me try, let me try. Here is the result of running the Check command, reformatted for readability:
a_sketchy_characterization_of_list_map list_map list_map_satisfies_the_specification_of_list_map nat nat
(fun n : nat => S n)
: list_map nat nat (fun n : nat => S n) nil = nil
/\
(forall v3 : nat,
list_map nat nat (fun n : nat => S n) (v3 :: nil) = S v3 :: nil)
/\
(forall v2 v3 : nat,
list_map nat nat (fun n : nat => S n) (v2 :: v3 :: nil) = S v2 :: S v3 :: nil)
/\
(forall v1 v2 v3 : nat,
list_map nat nat (fun n : nat => S n) (v1 :: v2 :: v3 :: nil) = S v1 :: S v2 :: S v3 :: nil)
Anton: Thanks, Pablito.
Alfrothul: It looks like the same as in Exercise 02.a, except that we map the successor function, not the identity function.
Dana: I agree. Shall we look at Exercise 02.c?
Alfrothul: Let’s.
Pablito (diligent): Here is the result of running the Check command, reformatted for readability:
fun V : Type =>
a_sketchy_characterization_of_list_map list_map list_map_satisfies_the_specification_of_list_map V V (fun v : V => v)
: forall V : Type,
list_map V V (fun v : V => v) nil = nil
/\
(forall v3 : V,
list_map V V (fun v : V => v) (v3 :: nil) = v3 :: nil)
/\
(forall v2 v3 : V,
list_map V V (fun v : V => v) (v2 :: v3 :: nil) = v2 :: v3 :: nil)
/\
(forall v1 v2 v3 : V,
list_map V V (fun v : V => v) (v1 :: v2 :: v3 :: nil) = v1 :: v2 :: v3 :: nil)
Alfrothul: It looks like the same as in Exercise 02.a, except that nat is generalized to any V.
Anton: So, a polymorphic function that copies a list stated as as an instance of list_map?
Dana: Otherwise known as list_copy_map, yes.
Given two types V and W, a value n of type W (the nil case), a function c of type V -> W -> W (the cons case), and a list of elements of V, list_fold_right homomorphically applies c to each successive element of the list and to the result of applying list_fold_right to the rest of the list. (N.B.: “homomorphic” means “structure-preserving”.) The following property captures this characterization for all the lists of length 0 to 3:
Property a_sketchy_characterization_of_list_fold_right :
forall list_fold_right : forall V W : Type, W -> (V -> W -> W) -> list V -> W,
specification_of_list_fold_right list_fold_right ->
forall (V W : Type)
(n : W)
(c : V -> W -> W),
( list_fold_right V W n c nil = n)
/\
(forall v3 : V,
list_fold_right V W n c (v3 :: nil) = c v3 n)
/\
(forall v2 v3 : V,
list_fold_right V W n c (v2 :: v3 :: nil) = c v2 (c v3 n))
/\
(forall v1 v2 v3 : V,
list_fold_right V W n c (v1 :: v2 :: v3 :: nil) = c v1 (c v2 (c v3 n))).
Prove Property a_sketchy_characterization_of_list_fold_right.
Characterize the following computations:
Given V : Type, W is nat, n is 0, and c is (fun (v : V) (ih : nat) => S ih):
Check (fun (V : Type) =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
nat
0
(fun (v : V) (ih : nat) => S ih)).
Given V : Type, W is list V, n is nil, and c is cons:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
(list V)
nil
(fun (v : V) (ih : list V) => v :: ih)).
Given V : Type and v2s : list V, W is list V, n is v2s, and c is cons:
Check (fun (V : Type)
(v2s : list V) =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
(list V)
v2s
(fun (v : V) (ih : list V) => v :: ih)).
Given V : Type, W is list (list V), n is nil, and c is fun (v : V) (ih : list (list V)) => (v :: nil) :: ih:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
(list (list V))
nil
(fun (v : V) (ih : list (list V)) => (v :: nil) :: ih)).
Given V : Type, W is list (V * V), n is nil, and c is fun (v : V) (ih : list (V * V)) => (v, v) :: ih:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
(list (V * V))
nil
(fun (v : V) (ih : list (V * V)) => (v, v) :: ih)).
Given V : Type, W : Type, and cons_case : V -> W -> W, W is V -> V, n is the identity function, and c is fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w):
Check (fun (V W : Type)
(cons_case : V -> W -> W) =>
a_sketchy_characterization_of_list_fold_right
list_fold_right
list_fold_right_satisfies_the_specification_of_list_fold_right
V
(W -> W)
(fun w : W => w)
(fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w))).
Food for thought: Given v and ih, fun w => ih (cons_case v w)) is the (function) composition of ih and cons_case v.
Given two types V and W, a value n of type W (the nil case), a function c of type V -> W -> W (the cons case), and a list of elements of V, list_fold_left homomorphically accumulates the application of c to each successive element of the list, starting with n. (N.B.: “homomorphic” means “structure-preserving”.) The following property captures this characterization for all the lists of length 0 to 3:
Property a_sketchy_characterization_of_list_fold_left :
forall list_fold_left : forall V W : Type, W -> (V -> W -> W) -> list V -> W,
specification_of_list_fold_left list_fold_left ->
forall (V W : Type)
(n : W)
(c : V -> W -> W),
( list_fold_left V W n c nil = n)
/\
(forall v3 : V,
list_fold_left V W n c (v3 :: nil) = c v3 n)
/\
(forall v2 v3 : V,
list_fold_left V W n c (v2 :: v3 :: nil) = c v3 (c v2 n))
/\
(forall v1 v2 v3 : V,
list_fold_left V W n c (v1 :: v2 :: v3 :: nil) = c v3 (c v2 (c v1 n))).
Prove Property a_sketchy_characterization_of_list_fold_left.
Characterize the following computations:
Given V : Type, W is nat, n is 0, and c is (fun (v : V) (ih : nat) => S ih):
Check (fun (V : Type) =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
nat
0
(fun (v : V) (ih : nat) => S ih)).
Given V : Type, W is list V, n is nil, and c is cons:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
(list V)
nil
(fun (v : V) (ih : list V) => v :: ih)).
Given V : Type and v2s : list V, W is list V, n is v2s, and c is cons:
Check (fun (V : Type)
(v2s : list V) =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
(list V)
v2s
(fun (v : V) (ih : list V) => v :: ih)).
Given V : Type, W is list (list V), n is nil, and c is fun (v : V) (ih : list (list V)) => (v :: nil) :: ih:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
(list (list V))
nil
(fun (v : V) (ih : list (list V)) => (v :: nil) :: ih)).
Given V : Type, W is list (V * V), n is nil, and c is fun (v : V) (ih : list (V * V)) => (v, v) :: ih:
Check (fun V : Type =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
(list (V * V))
nil
(fun (v : V) (ih : list (V * V)) => (v, v) :: ih)).
Given V : Type, W : Type, and cons_case : V -> W -> W, W is V -> V, n is the identity function, and c is fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w):
Check (fun (V W : Type)
(cons_case : V -> W -> W) =>
a_sketchy_characterization_of_list_fold_left
list_fold_left
list_fold_left_satisfies_the_specification_of_list_fold_left
V
(W -> W)
(fun w : W => w)
(fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w))).
Food for thought: Given v and ih, fun w => ih (cons_case v w)) is the (function) composition of ih and cons_case v.
Dana: Hmm...
Alfrothul: Yes, Dana?
Dana: Remember monoids?
Bong-sun: Let me see... A set together with a binary operation that is associative and such that one of the elements of the set is neutral for the binary operation?
Dana: Yes. And the element that is neutral is said to be an identity element.
Alfrothul (brightly): For example, lists form a monoid, with list_append as the binary operation and nil as the identity element.
Bong-sun: You seem to have something in mind, Dana.
Dana: I do. Endofunctions – that is to say, functions with the same domain and codomain – also form a monoid, with function composition as the binary operation and the identity function as the identity element.
Alfrothul: So?
Dana: Well, in Exercise 04.f and in Exercise 06.f, list_fold_right and list_fold_left map lists to endofunctions.
Bong-sun (practical): Well, they implement homomorphisms, so they map a monoid to another monoid.
Halcyon: Headache!
Alfrothul (kindly): Being homomorphic just means being structure-preserving.
Bong-sun: Right. So they map nil to the identity function and cons to the composition of two functions.
Dana (reflective): I wonder what would happen if we swapped the two functions that are being composed...
Bong-sun: You mean fun w => ih (cons_case v w)) rather than fun w => cons_case v (ih w))?
Dana: Yes. That should defeat the idea of the simulation.
Pablito: Let me try! Let me try! <clickety clickety click>
Halcyon: O.M.G.
Loki: Yes?
Fixed a typo in Exercise 02.e, thanks to Vikram Goyal’s eagle eye [27 Mar 2025]
Fine-tuned Exercise 02, Exercise 04, and Exercise 06, provided solutions for Exercise 02.a, Exercise 02.b, and Exercise 02.c, and added the postlude [23 Mar 2025]
Created [22 Mar 2025]