The goal of this lecture note is to introduce the polymorphic map function that given a function and a list, applies this function to each of the elements of this list and collects the results in a new list. We had seen an instance of the map function for strings in Week 05, Exercise 1.
Anakin (opening really big eyes): Is it possible to use this expressive power?The Supreme Chancellor: Not with a for loop.
Our task is to implement an OCaml function that, given a list of integers, maps it to a list of integers containing the successors of all the elements of the given list, in the same order:
let test_list_map_succ candidate =
(candidate [2; 1; 0] = [3; 2; 1])
(* etc. *);;
Clearly this function should be specified by induction over its argument ns:
base case: ns = []
the empty list containing no elements, this function should map it to the empty list
induction step: ns = n :: ns'
assuming that the function maps ns' to the corresponding list of successors, which is the induction hypothesis, it should map n :: ns' to the list that starts with succ n and continues with this corresponding list of successors
Based on this specification, we can flesh out the unit-test function:
let test_list_map_succ candidate =
(* an instance of the base case: *)
let bc = (candidate [] = [])
(* a few handpicked lists: *)
and b1 = (candidate [0] = [1])
and b2 = (candidate [1; 0] = [2; 1])
and b3 = (candidate [2; 1; 0] = [3; 2; 1])
and b4 = (candidate [3; 2; 1; 0] = [4; 3; 2; 1])
(* an instance of the induction step: *)
and is = (let n = 4
and ns' = [3; 2; 1; 0]
in let ih = candidate ns'
in candidate (n :: ns') = succ n :: ih)
(* etc. *)
in bc && b1 && b2 && b3 && b4 && is;;
Since list_map_succ is specified inductively, it is to be programmed as a structurally recursive function. Here is its skeleton:
let list_map_succ ns =
let rec visit ns =
match ns with
| [] ->
...
| n :: ns' ->
let ih = visit ns'
in ...
in visit ns;;
Rationale: the skeleton of visit follows the inductive structure of lists, i.e., it has a base case (the argument is the empty list) and an induction step (the argument is not the empty list).
Now all we need is to fill the blanks:
To wit:
let list_map_succ_v0 ns =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
let ih = visit ns'
in succ n :: ih
in visit ns;;
This implementation is structurally recursive (since it follows the inductive structure of its input) and it passes the unit test:
# test_list_map_succ list_map_succ_v0;;
- : bool = true
#
In the induction step, the let-expression that declares ih, in the definition of visit, is cosmetic and so we can unfold it:
let list_map_succ_v1 ns =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
(succ n) :: (visit ns')
in visit ns;;
This simplified implementation is still structurally recursive and it passes the unit test:
# test_list_map_succ list_map_succ_v1;;
- : bool = true
#
Our task is to implement an OCaml function that, given a list of integers, maps it to a list of integers containing the predecessors of all the elements of the given list, in the same order:
let test_list_map_pred candidate =
let b0 = (candidate [3; 2; 1] = [2; 1; 0])
and b1 = (candidate [2; 1; 0] = [1; 0; ~-1])
(* etc. *)
in b0 && b1;;
...
Our task is to implement an OCaml function that, given a list of integers, maps it to a list of integers containing the squares of all the elements of the given list, in the same order:
let test_list_map_square candidate =
(candidate [3; 2; 1] = [9; 4; 1])
(* etc. *);;
...
Our task is to implement an OCaml function that, given a list of integers, maps it to a list of integers containing the singleton list of all the elements of the given list, in the same order:
let test_list_map_singleton candidate =
(candidate [3; 2; 1] = [[3]; [2]; [1]])
(* etc. *);;
...
Generalizing, let us write a generic version of the functions above, list_map, that is parameterized by the function to map. This generic function is still specified by induction over its argument ns, given a function f:
base case: ns = []
the empty list containing no elements, this function should map it to the empty list
induction step: ns = n :: ns'
assuming that the function maps ns' to the corresponding list of successors, which is the induction hypothesis, it should map n :: ns' to the list that starts with f n and continues with this corresponding list of successors
Since list_map is specified inductively, it is to be programmed as a structurally recursive function. Here is its skeleton:
let list_map f ns =
let rec visit ns =
match ns with
| [] ->
...
| n :: ns' ->
let ih = visit ns'
in ...
in visit ns;;
Rationale: the skeleton of visit follows the inductive structure of lists, i.e., it has a base case (the argument is the empty list) and an induction step (the argument is not the empty list).
Now all we need is to fill the blanks:
To wit:
let list_map_v0 f ns =
(* list_map : ('a -> 'b) -> 'a list -> 'b list *)
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
let ih = visit ns'
in f n :: ih
in visit ns;;
This implementation is structurally recursive (since it follows the inductive structure of its input) and we can instantiate it to implement each of the warmup examples above:
let list_map_succ_v2 = list_map_v0 succ;;
let list_map_pred_v2 = list_map_v0 pred;;
let list_map_square_v2 = list_map_v0 (fun n -> n * n);;
let list_map_singleton_v2 = list_map_v0 (fun n -> [n]);;
All these implementations pass the corresponding unit tests:
# test_list_map_succ list_map_succ_v2;;
- : bool = true
# test_list_map_pred list_map_pred_v2;;
- : bool = true
# test_list_map_square list_map_square_v2;;
- : bool = true
# test_list_map_singleton list_map_singleton_v2;;
- : bool = true
#
This generic map function is available in OCaml’s List library:
# test_list_map_succ (List.map succ);;
- : bool = true
# test_list_map_pred (List.map pred);;
- : bool = true
# test_list_map_square (List.map (fun n -> n * n));;
- : bool = true
# test_list_map_singleton (List.map (fun n -> [n]);;
- : bool = true
#
A map function implements a homomorphism, i.e., it preserves the structure of its input.
Implement the list analogue of String.mapi so that:
# list_mapi (fun n v -> (n, v)) ['a'; 'b'; 'c'];;
- : (int * char) list = [(0, 'a'); (1, 'b'); (2, 'c')]
#
Use this analogue to implement the polymorphic identity function over lists.
Use this analogue to implement a polymorphic function that maps a list to a matching list of increasing indices. For example, this function should map the list ['a'; 'b'; 'c'] to [0; 1; 2].
Use this analogue to implement a polymorphic function that maps a list to a matching list of decreasing indices. For example, this function should map the list ['a'; 'b'; 'c'] to [2; 1; 0].
In the particular case where the function to map over a list is a predicate (i.e., a Boolean-valued function), we often want to compute not the list of its results but their conjunction or their disjunction:
let list_andmap p vs =
(* list_andmap : ('a -> bool) -> 'a list -> bool *)
let rec visit vs =
match vs with
| [] ->
true
| v :: vs' ->
p v && visit vs'
in visit vs;;
let list_ormap p vs =
(* list_ormap : ('a -> bool) -> 'a list -> bool *)
let rec visit vs =
match vs with
| [] ->
false
| v :: vs' ->
p v || visit vs'
in visit vs;;
Rationale:
In this case, it is critical not to name the recursive call to visit so that list_andmap and list_ormap benefit from short-circuit evaluation:
# list_andmap (fun n -> if n = 0 then false else 1/0 = 0) [0; 1; 2; 3];;
- : bool = false
# list_ormap (fun n -> if n = 0 then true else 1/0 = 0) [0; 1; 2; 3];;
- : bool = true
#
Indeed, suppose we named the recursive call to visit, as in the incorrect definition below:
let list_andmap_incorrect p vs =
(* list_andmap_incorrect : ('a -> bool) -> 'a list -> bool *)
let rec visit vs =
match vs with
| [] ->
true
| v :: vs' ->
let ih = visit vs'
in p v && ih
in visit vs;;
Then, if p denotes fun n -> if n = 0 then false else 1/0 = 0, desugaring list_andmap_incorrect p [0; 1] would yield:
let ih = let ih = true
in p 1 && ih
in p 0 && ih;;
Evaluating this expression would give rise to the error Division_by_zero because p 1 is evaluated first, whereas evaluating p 0 && p 1 && true would yield false because p 0 is evaluated first and OCaml implements short-circuit Boolean evaluation. Indeed evaluating p 0 yields false, and therefore the result of evaluating p 0 && p 1 && true is false, without p 1 && true being evaluated (which would give rise to the error Division_by_zero).
Harald: I am so reminded of the midterm project.Alfrothul: You and me both, Harald. You and me both.
The desugared counterparts of list_andmap p [v1; v2; v3; ...; vN] and list_ormap p [v1; v2; v3; ...; vN] read p v1 && p v2 && p v3 && ... && p vN && true and p v1 || p v2 || p v3 || ... || p vN || false, but it would be more intuitive for them to read:
p v1 && p v2 && p v3 && ... && p vN
p v1 || p v2 || p v3 || ... || p vN
without the trailing && true and || false. Not only would it be more intuitive, but it would have the property that the calls p vN would be tail calls, i.e., the last thing that happens when applying list_andmap and list_ormap.
Long story short: to define such tail-sensitive versions of list_andmap and list_ormap, one should define them by induction over the tail of their input list when this list is nonempty:
let list_andmap_tail_sensitive p vs =
(* list_andmap_tail_sensitive : ('a -> bool) -> 'a list -> bool *)
match vs with
| [] ->
true
| v :: vs' ->
let rec visit v vs =
match vs with
| [] ->
p v
| v' :: vs' ->
p v && visit v' vs'
in visit v vs';;
let list_ormap_tail_sensitive p vs =
(* list_ormap_tail_sensitive : ('a -> bool) -> 'a list -> bool *)
match vs with
| [] ->
true
| v :: vs' ->
let rec visit v vs =
match vs with
| [] ->
p v
| v' :: vs' ->
p v || visit v' vs'
in visit v vs';;
The point is that when the tail of a list is empty, its head is the last element of this list.
Fixed the access to the resource file, thanks to Le Tram Anh’s eagle eye [15 Mar 2020]
Created [14 Mar 2020]