The goal of this lecture note is to explore the two patterns of structural recursion for lists: one, recursive, and the other, tail recursive and with an accumulator.
Let us revisit the template for any structurally recursive function over lists. It follows the inductive structure of lists – base case and induction step:
let ... vs_init =
let rec traverse vs =
match vs with
| [] ->
...
| v :: vs' ->
let ih = traverse vs'
in ...
in traverse vs_init;;
Let us functionally abstract what to do in the base case and what to do in the induction step. The result is what is called the fold-right function for lists (traditionally called just fold_right in practice):
let fold_right_list nil_case cons_case vs_init =
(* fold_right_list : 'a -> ('b -> 'a -> 'a) -> 'b list -> 'a *)
let rec traverse vs =
(* traverse : 'b list -> 'a *)
match vs with
| [] ->
nil_case
| v :: vs' ->
let ih = traverse vs'
in cons_case v ih
in traverse vs_init;;
Given a nil case nil_specific, a cons case cons_specific, and a list v0 :: v1 :: v2 :: v3 :: [], which was constructed by evaluating:
List.cons v0 (List.cons v1 (List.cons v2 (List.cons v3 [])))
fold_right_list essentially yields the result of evaluating:
cons_specific v0 (cons_specific v1 (cons_specific v2 (cons_specific v3 nil_specific)))
In words, the result of fold_right_list is a series of nested applications of cons_specific that mimics the nested occurrences of the original constructor List.cons in the given list.
Here is how we had defined the length function:
let length vs_init =
let rec measure vs =
match vs with
| [] ->
0
| v :: vs' ->
let ih = measure vs'
in succ ih
in measure vs_init;;
(As usual, the induction hypothesis is implemented by the recursive call.)
By instantiating nil_case to be 0 and cons_case to be (fun v ih -> succ ih), we make fold_right_list emulate the computation of the length function:
let length_alt vs =
fold_right_list 0
(fun v ih ->
1 + ih)
vs;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined an unparsing function for polymorphic lists in long hand:
let show_list_in_long_hand show_yourself vs_init =
(* show_list_in_long_hand : ('a -> string) -> 'a list -> string *)
let rec visit vs =
match vs with
| [] ->
"[]"
| v :: vs' ->
let ih = visit vs'
in (show_yourself v) ^ " :: " ^ ih
in visit vs_init;;
By instantiating nil_case to be "[]" and cons_case to be (fun v ih -> (show_yourself v) ^ " :: " ^ ih), we make fold_right_list emulate the computation of the unparsing function for lists in long hand:
let show_list_in_long_hand_alt show_yourself vs_init =
(* show_list_in_long_hand_alt : ('a -> string) -> 'a list -> string *)
fold_right_list "[]"
(fun v ih ->
(show_yourself v) ^ " :: " ^ ih)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined an unparsing function for polymorphic lists in short hand:
let show_list_in_short_hand show_yourself vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_yourself v) ^ (let rec show_list_aux vs =
(* show_list_aux : 'a list -> string *)
match vs with
| [] ->
"]"
| v :: vs' ->
let ih = show_list_aux vs'
in "; " ^ (show_yourself v) ^ ih
in show_list_aux vs');;
By instantiating nil_case to be "]" and cons_case to be (fun v ih -> "; " ^ (show_yourself v) ^ ih), we make fold_right_list emulate the computation of the unparsing function for lists in short hand:
let show_list_in_long_hand_alt show_yourself vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_yourself v) ^ (fold_right_list "]"
(fun v ih ->
"; " ^ (show_yourself v) ^ ih)
vs');;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function that duplicates the elements of any given list:
let stutter2 vs_init =
(* stutter2 : 'a list -> 'a list *)
let rec visit vs =
(* visit : 'a list -> 'a list *)
match vs with
| [] ->
[]
| v :: vs' ->
let ih = visit vs'
in v :: v :: ih
in visit vs_init;;
By instantiating nil_case to be [] and cons_case to be (fun v ih -> v :: v :: ih), we make fold_right_list emulate the computation of the stutter2 function:
let stutter2_alt vs_init =
fold_right_list []
(fun v ih ->
v :: v :: ih)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function to concatenate lists:
let append xs_init ys_init =
let rec visit xs =
match xs with
| [] ->
ys_init
| x :: xs' ->
let ih = visit xs'
in x :: ih
in visit xs_init;;
Given two lists xs_init and ys_init, by instantiating nil_case to be ys_init and cons_case to be (fun x ih -> x :: ih), we make fold_right_list emulate the computation of the append function:
let append_alt xs_init ys_init =
fold_right_list ys_init
(fun x ih ->
x :: ih)
xs_init;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function to test whether an element occurs in a list:
let member e es_init =
let rec visit es =
match es with
| [] ->
false
| e' :: es' ->
let ih = visit es'
in if e = e'
then true
else ih
in visit es_init;;
Given an element e and a list es_init, by instantiating nil_case to be false and cons_case to be (fun e' ih -> if e = e' then true else ih), we make fold_right_list emulate the computation of the member function:
let member_alt e es_init =
fold_right_list false
(fun e' ih ->
if e = e'
then true
else ih)
es_init;;
This alternative implementation passes the corresponding unit tests.
Given a list, what happens if we instantiate nil_case to be [] and cons_case to be (fun x ih -> x :: ih), i.e., List.cons? Which function does fold_right_list emulate then?
In other words, you are asked to characterize the following OCaml function:
let the_following_OCaml_function xs =
fold_right_list [] (fun x ih -> x :: ih) xs;;
As an unashamed excuse for writing structurally recursive functions over lists using fold_right_list, let us revisit the representation of sets as the list of their elements (without repetition).
Revisit Exercise 4 in the lecture note about representing sets as lists, and express your set_union function using fold_right_list. Verify that it passes the unit tests.
Willy nilly, one defines set union by induction on its first argument:
let set_union e1s e2s =
let rec visit e1s =
match e1s with
| [] ->
e2s
| e1 :: e1s' ->
let ih = visit e1s'
in if belongs_to e1 e2s
then ih
else e1 :: ih
in visit e1s;;
By instantiating nil_case to be e2s and cons_case to be (fun e1 ih -> if belongs_to e1 e2s then ih else e1 :: ih), we make fold_right_list emulate the computation of the set_union function:
let set_union_alt e1s e2s =
fold_right_list e2s
(fun e ih ->
if belongs_to e e2s
then ih
else e :: ih)
e1s;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 6 in the lecture note about representing sets as lists, and express your set_intersection function using fold_right_list. Verify that it passes the unit tests.
Revisit Exercise 9 in the lecture note about representing sets as lists, and express your set_minus function using fold_right_list. Verify that it passes the unit tests.
Revisit Exercise 12 in the lecture note about representing sets as lists, and express your set_minus_symmetric function using fold_right_list. Verify that it passes the unit tests.
Here is how we had defined a function that computes the Cartesian product of two sets represented as the list of their elements:
let cartesian_product_2 vs_init ws_init =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_inner = traverse_2 ws'
in (v, w) :: ih_inner
in traverse_2 ws_init
in traverse_1 vs_init;;
We can express traverse_2 using fold_right_list by instantiating nil_case to be ih_outer and cons_case to be (fun w ih_inner -> (v, w) :: ih_inner):
let cartesian_product_2_alt' vs_init ws_init =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in fold_right_list ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_init
in traverse_1 vs_init;;
This alternative implementation passes the corresponding unit tests.
We can express traverse_1 using fold_right_list by instantiating nil_case to be [] and cons_case to be (fun v ih_outer -> fold_right_list ih_outer (fun w ih_inner -> (v, w) :: ih_inner) ws_init):
let cartesian_product_2_alt vs_init ws_init =
fold_right_list []
(fun v ih_outer ->
fold_right_list ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_init)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function that computes the Cartesian product of three sets represented as the list of their elements:
let cartesian_product_3 vs_init ws_init xs_init =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_median = traverse_2 ws'
in let rec traverse_3 xs =
match xs with
| [] ->
ih_median
| x :: xs' ->
let ih_inner = traverse_3 xs'
in (v, w, x) :: ih_inner
in traverse_3 xs_init
in traverse_2 ws_init
in traverse_1 vs_init;;
We can express traverse_3 using fold_right_list by instantiating nil_case to be ih_median and cons_case to be (fun x ih_inner -> (v, w, x) :: ih_inner):
let cartesian_product_3_alt'' vs_init ws_init xs_init =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_median = traverse_2 ws'
in fold_right_list ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_init
in traverse_2 ws_init
in traverse_1 vs_init;;
This alternative implementation passes the corresponding unit tests.
We can express traverse_2 using fold_right_list by instantiating nil_case to be ih_outer and cons_case to be (fun w ih_inner -> fold_right_list ih_median (fun x ih_inner -> (v, w, x) :: ih_inner) xs_init):
let cartesian_product_3_alt' vs_init ws_init xs_init =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in fold_right_list ih_outer
(fun w ih_median ->
fold_right_list ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_init)
ws_init
in traverse_1 vs_init;;
This alternative implementation passes the corresponding unit tests.
We can express traverse_1 using fold_right_list by instantiating nil_case to be [] and cons_case to be (fun v ih_outer -> fold_right_list ih_outer (fun w ih_inner -> fold_right_list ih_median (fun x ih_inner -> (v, w, x) :: ih_inner) xs_init) ws_init):
let cartesian_product_3_alt vs_init ws_init xs_init =
fold_right_list []
(fun v ih_outer ->
fold_right_list ih_outer
(fun w ih_median ->
fold_right_list ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_init)
ws_init)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 15 in the lecture notes about the Cartesian product and express your cartesian_product_4 function using fold_right_list. Verify that it passes the unit tests.
Let us revisit the template for any structurally recursive function over lists that uses an accumulator. It follows the inductive structure of lists – base case and induction step:
let ... vs_init =
let rec traverse vs a =
match vs with
| [] ->
a
| v :: vs' ->
traverse vs' ...
in traverse vs_init ...;;
Let us functionally abstract what to do in the base case and what to do in the induction step. The result is what is called the fold-left function for lists (traditionally called just fold_left in practice):
let fold_left_list nil_case cons_case vs_init =
(* fold_left_list : 'a -> ('b -> 'a -> 'a) -> 'b list -> 'a *)
let rec traverse vs a =
(* traverse : 'b list -> 'a *)
match vs with
| [] ->
a
| v :: vs' ->
traverse vs' (cons_case v a)
in traverse vs_init nil_case;;
Given a nil case nil_specific, a cons case cons_specific, and a list v0 :: v1 :: v2 :: v3 :: [], which was constructed by evaluating:
List.cons v0 (List.cons v1 (List.cons v2 (List.cons v3 [])))
fold_left_list essentially yields the result of evaluating:
cons_specific v3 (cons_specific v2 (cons_specific v1 (cons_specific v0 nil_specific)))
In words, the result of fold_left_list is a series of nested applications of cons_specific that mirrors the nested occurrences of the original constructor List.cons in the given list.
Here is how we had defined the length function using an accumulator:
let length_acc vs_init =
let rec measure vs a =
match vs with
| [] ->
a
| v :: vs' ->
measure vs' (1 + a)
in measure vs_init 0;;
By instantiating nil_case to be 0 and cons_case to be (fun v a -> succ a), we make fold_left_list emulate the computation of the length_acc function:
let length_acc_alt vs =
fold_left_list 0
(fun v a ->
succ a)
vs;;
This alternative implementation passes the corresponding unit tests.
Given a list xs, what happens if we instantiate nil_case to be [] and cons_case to be (fun x a -> x :: a)? Which function does fold_left_list emulate then?
In other words, you are asked to characterize the following other OCaml function:
let the_following_other_OCaml_function xs =
fold_left_list [] (fun x a -> x :: a) xs;;
As an unashamed excuse for writing structurally recursive functions over lists that use an accumulator using fold_left_list, let us re3visit the representation of sets as the list of their elements (without repetition).
Revisit Exercise 3 in the lecture note about programming with lists using accumulators and express your set_union_acc function using fold_left_list.
Verify that it passes the unit tests.
We had defined set union by induction on its first argument:
let set_union_acc e1s_init e2s_init =
let rec visit e1s a =
match e1s with
| [] ->
a
| e1 :: e1s' ->
visit e1s' (if belongs_to e1 e2s_init
then a
else e1 :: a)
in visit e1s_init e2s_init;;
By instantiating nil_case to be e2s_init and cons_case to be (fun e1 a -> if belongs_to e1 e2s_init then a else e1 :: a), we make fold_left_list emulate the computation of the set_union_acc function:
let set_union_acc_alt e1s_init e2s_init =
fold_left_list e2s_init
(fun e1 a ->
if belongs_to e1 e2s_init
then a
else e1 :: a)
e1s_init;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 4 in the lecture note about programming with lists using accumulators and express your set_intersection_acc function using fold_left_list.
Verify that it passes the unit tests.
Revisit Exercise 5 in the lecture note about programming with lists using accumulators and express your set_minus_acc function using fold_left_list.
Verify that it passes the unit tests.
Revisit Exercise 5 in the lecture note about programming with lists using accumulators and express your symmetric_set_minus_acc function using fold_left_list.
Verify that it passes the unit tests.
Since map_list is structurally recursive, it can be defined using fold_right_list:
let map_list_v2 f ns =
fold_right_list [] (fun n ih -> f n :: ih) ns;;
To wit:
# map_list_v2 succ [1; 2; 3];;
- : int list = [2; 3; 4]
#
Not so, though, for andmap and ormap, since they critically rely on OCaml’s short-circuit evaluation for Boolean operations:
# let andmap_not p vs = fold_right_list true (fun v ih -> p v && ih) vs;;
val andmap_not : ('a -> bool) -> 'a list -> bool = <fun>
# andmap_not (fun n -> if n = 0 then false else 1/0 = 0) [0; 1; 2; 3];;
Exception: Division_by_zero.
#
Harald: I feel exhausted.
Alfrothul: Still.
Harald: Still, what.
Alfrothul: Doesn’t it look like fold_right_list and fold_left_list are just one list reversal away from another?
Harald: You mean that for any n, c, and vs of the right types, evaluating fold_right_list n c vs and fold_left_list n c (List.rev vs) yield the same result?
Alfrothul: What I actually was thinking of was that evaluating fold_right_list n c vs and List.rev (fold_left_list n c vs) yield the same result, but otherwise yes.
Brynja (perspicacious): Assuming the result to be a list.
Vigfus: Actually, fold_right_list n c (List.rev vs) and fold_left_list n c vs would fit the bill too.
Brynja: Or List.rev (fold_right_list n c vs) and fold_left_list n c vs for that matter, if the result is a list, but how about we call it a day.
Halcyon: You are all welcome to have a seat.
Harald (hastily): And that means you too, Mimer.
Brynja (amused): Too late.
In the light of this aftermath, it doesn’t really matter whether to use fold_left_list or fold_right_list to compute, e.g., set union with an accumulator (as in Exercise 14) or without (as in Exercise 8), since the order of elements doesn’t matter in a list that represents a set.
However, it does matter when expressing the functions computing the Cartesian products, because using fold_left_list instead of fold_right_list makes the unit tests fail:
# let cartesian_product_2_alt' vs_init ws_init =
fold_left_list []
(fun v ih_outer ->
fold_left_list ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_init)
vs_init;;
val cartesian_product_2_alt' : 'a list -> 'b list -> ('a * 'b) list = <fun>
# let () = assert (test_cartesian_product_2 cartesian_product_2_alt');;
Exception: Assert_failure ("//toplevel//", 638, 9).
#
Why is that? What needs to be fixed?
This exercise is due to Christopher Strachey.
Implement an OCaml function that generalizes cartesian_product_2 and cartesian_product_3 in that when applied to a list of sets, it returns their Cartesian product (as a list of lists instead of as a list of tuples):
let cartesian_product_star nss =
(* cartesian_product_star : 'a list list -> 'a list list *)
match nss with
| [] ->
[[]]
| n1s :: [] ->
List.map (fun x1 -> [x1]) n1s
| n1s :: n2s :: [] ->
List.map (fun (x1, x2) -> [x1; x2]) (cartesian_product_2 n1s n2s)
| n1s :: n2s :: n3s :: [] ->
List.map (fun (x1, x2, x3) -> [x1; x2; x3]) (cartesian_product_3 n1s n2s n3s)
| _ ->
let () = assert false
in [];;
Vigfus: Remember the implementation of powerset_v1?
Harald: The listless one? Yes:
let append_map f vs rest =
let rec visit vs =
match vs with
| [] ->
rest
| v :: vs' ->
f v :: visit vs'
in visit vs;;
let powerset_v1 vs_init =
let rec visit vs =
match vs with
| [] ->
[[]]
| v :: vs' ->
let ih = visit vs'
in append_map (fun ws -> v :: ws) ih ih
in visit vs_init;;
Alfrothul: You tested it:
# test_powerset_int powerset_v1;;
- : bool = true
#
Vigfus: I did. But this implementation, is it structurally recursive?
Harald: Well, yes – its recursive calls follow the structure of its input data. Why do you ask?
Vigfus: The induction hypothesis is used twice.
Alfrothul: And so it is. But we could still express it using fold_right_list.
Brynja: Yay, more generic programming.
Vigfus: May I give it a shot?
Alfrothul: By all means.
Vigfus: Lemmesee:
let powerset_v2 vs_init =
fold_right_list
[[]]
(fun v ih ->
append_map (fun ws -> v :: ws) ih ih)
vs_init;;
Harald (courteously): Testing, testing:
# test_powerset_int powerset_v2;;
- : bool = true
#
Alfrothul: Wait a minute. The definition of append_map' is structurally recursive too.
Harald: True. Look:
let append_map' f vs rest =
fold_right_list
rest
(fun v ih ->
f v :: ih)
vs;;
Vigfus: Just a sec:
# test_append_map_int append_map';;
- : bool = true
#
Alfrothul: How about we unfold the call to append_map' in the definition of powerset_v2?
Harald (reflexively): Unfold the call to append_map' in the definition of powerset_v2.
Alfrothul: Yes, look:
let powerset_v7 vs_init =
fold_right_list
[[]]
(fun v vss ->
fold_right_list
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_init;;
Harald: Harumph. You, my friend, have been skipping a few derivation steps.
Alfrothul (virtuously): But they are spelled out in the accompanying resource file.
Vigfus (with uncertainty): Testing, testing:
# test_powerset_int powerset_v7;;
- : bool = true
#
Vigfus (to himself): Wow.
Mimer: According to Michael Gordon, this definition was discovered by Dave du Feu, back in the days.
Brynja (wondering): When a list represents a set, the order of its elements does not matter, right?
Harald: Right.
Brynja: So we could use fold_left_list instead of fold_right_list, couldn’t we?
Alfrothul: That is going to change the order of elements in the resulting lists and sublists, but the result should be indeed correct.
Harald: For example, all the sublists will be in reverse order.
Brynja: So we need a new unit-test function:
let test_powerset_int' candidate =
let test vs =
set_equal (candidate vs) (List.map List.rev (powerset_v7 vs))
in let b0 = test []
and b1 = test [1]
and b2 = test [2; 1]
and b3 = test [3; 2; 1]
and b4 = test [4; 3; 2; 1]
and b5 = test [5; 4; 3; 2; 1]
and b6 = test [6; 5; 4; 3; 2; 1]
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
Alfrothul: I see – the sublists are reversed and the order of the lists is left to set_equal. Let’s do this:
let powerset_v7' vs_init =
fold_left_list
[[]]
(fun v vss ->
fold_left_list
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_init;;
Vigfus (hanging on): Testing again:
# test_powerset_int' powerset_v7';;
- : bool = true
#
Harald: I wonder how this function works.
Alfrothul: To discover that, we can unfold the two calls to fold_left_list and simplify. Skipping a few steps...
Harald: You don’t say.
Brynja (unrattled): They are spelled out in the accompanying resource file.
Alfrothul: ...we obtain the following tail-recursive definition:
let powerset_v0' vs_init =
let rec outer_loop vs outer_a =
match vs with
| [] ->
outer_a
| v :: vs' ->
let rec inner_loop vss inner_a =
match vss with
| [] ->
outer_loop vs' inner_a
| vs :: vss' ->
inner_loop vss' ((v :: vs) :: inner_a)
in inner_loop outer_a outer_a
in outer_loop vs_init [[]];;
Brynja: And a listless one too.
Harald: Renaming the outer instance of traverse as outer_loop and the innner instance as inner_loop makes sense.
Brynja: Ditto for the outer accumulator and the inner accumulator.
Vigfus (bravely): Testing, testing:
# test_powerset_int' powerset_v0';;
- : bool = true
#
Alfrothul (candidly): Man, I would be hard pressed to define powerset_v0' by hand in the first place.
Mimer: That’s another aspect of unfolding function calls.
Harald: What do you mean?
Mimer: In the chapter about Inlining functions, we have unfolded calls to a fold function to verify that we fall back on our feet when inlining its definition.
Alfrothul: But here we didn’t start from a structurally recursive function so we are not in position to fall back on our feet.
Mimer: True. But we are in position to discover the underlying iterative program that does the job. In doing so, we can indeed realize that inlining doesn’t merely make us fall back on our feet, as in Chapter about Inlining functions, it can make us discover a new program that we did not know yet, one that we can then wonder whether we could have written by hand in the first place, or that can suggest other programs.
Brynja: So Platonism is also at work in computer science, in that programs are not only invented, they can also be discovered?
Mimer: Indeed. Programs are not just things that we write independently of each other: they are things that we can relate to each other, that we can reason about using observational equivalence, and that we can derive from other programs, or from specifications, or from properties.
Fine-tuned the narrative [09 Jun 2019]
Added the generic version of powerset and its fold-left counterpart [19 May 2019]
Fixed two typos in the narrative, thanks to Yunjeong Lee’s eagle eye [02 May 2019]
Added the section on defining map_list generically as well as Exercise 19 and Exercise 20 [24 Mar 2019]
Created [17 Mar 2019]