The goal of this lecture note is to describe how to inline the definition of functions in function calls by unfolding these calls. Call unfolding is a useful tool to reason algebraically about OCaml programs. It makes it possible, for example, to consider nat_fold_right as syntactic sugar and verify that we fall back on our feet when inlining its definition.
Consider the function mapping a natural number n to the (n+1)th odd natural number:
let test_make_odd_number candidate =
let b0 = (candidate 0 = 1)
and b1 = (candidate 1 = 3)
and b2 = (candidate 2 = 5)
and b3 = (candidate 3 = 7)
(* etc. *)
in b0 && b1 && b2 && b3;;
let make_odd_number n =
2 * n + 1;;
Now say that the function mapping an integer n to the (n+1)th even natural number is defined in terms of make_odd_number:
let test_make_even_number candidate =
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 2)
and b2 = (candidate 2 = 4)
and b3 = (candidate 3 = 6)
(* etc. *)
in b0 && b1 && b2 && b3;;
let make_even_number_v0 m =
(make_odd_number m) - 1;;
Inlining make_odd_number yields:
let make_even_number_v1 m =
((fun n -> 2 * n + 1) m) - 1;;
Applying the function formerly denoted by make_odd_number yields:
let make_even_number_v2 m =
(let n = m in 2 * n + 1) - 1;;
This let-expression is just used for renaming a variable, so it is safe to unfold it:
let make_even_number_v3 m =
(2 * m + 1) - 1;;
Disregarding the possibility of integer overflow, the successive incrementation and decrementation cancel out:
let make_even_number_v4 m =
2 * m;;
And the result is the simple definition one would write by hand to start with.
N.B.: Each of the successive definitions pass the unit tests, which act as what is called “regression tests” – tests to check that each new version is still compatible with the previous versions.
Given a function:
let foo x y z =
...body of foo...;;
the call:
... (foo e1 e2 e3) ...
is unfolded as:
... ((fun x y z -> ...body of foo...) e1 e2 e3) ...
And applying the function formerly denoted by foo yields:
... (let z = e3
and y = e2
and x = e1
in ...body of foo...) ...
to respect the order in which expressions are evaluated in OCaml, as investigated in the mini-project about the underlying determinism of OCaml.
To verify that we fall back on our feet, we can desugar the instances of nat_fold_right by inlining its definition at its points of call:
let nat_fold_right zero_case succ_case n =
(* nat_fold_right : 'a -> ('a -> 'a) -> int -> 'a *)
let () = assert (n >= 0) in
let rec visit n =
if n = 0
then zero_case
else let n' = n - 1
in let ih = visit n'
in succ_case ih
in visit n;;
We had generically defined twice as:
let twice_v4 n =
nat_fold_right 0 (fun ih -> succ (succ ih)) n;;
Let us inline nat_fold_right, i.e., unfold its call, and conflate the standard two steps of (1) replacing nat_fold_right with its denotation and (2) applying this denotation:
let twice_v5 n =
let n = n
and succ_case = (fun ih -> succ (succ ih))
and zero_case = 0
in let () = assert (n >= 0) in
let rec visit n =
if n = 0
then zero_case
else let n' = n - 1
in let ih = visit n'
in succ_case ih
in visit n;;
The first clause of the let expression renames n to itself. The two last clauses declare values and they are linear. So let us unfold the let expression:
let twice_v6 n =
let () = assert (n >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in (fun ih -> succ (succ ih)) ih
in visit n;;
Applying (fun ih -> succ (succ ih)) yields:
let twice_v7 n =
let () = assert (n >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in let ih = ih
in succ (succ ih)
in visit n;;
The inner let-expression renames ih to itself, so we can unfold it:
let twice_v8 n =
let () = assert (n >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in succ (succ ih)
in visit n;;
The result coincides with the definition of twice_v3 in Week 05 (Section Simplifying the definition of the doubling function), and so we do fall back on our feet.
N.B.: Witness the accompanying resource file, for each of the successive definitions, we use the unit tests as regression tests.
We had generically defined add as:
let add_v4 x y =
nat_fold_right y succ x;;
Let us inline the call to nat_fold_right (again, conflating the standard two steps of replacing nat_fold_right with its denotation and applying this denotation):
let add_v5 x y =
let n = x
and succ_case = succ
and zero_case = y
in let () = assert (n >= 0) in
let rec visit n =
if n = 0
then zero_case
else let n' = n - 1
in let ih = visit n'
in succ_case ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let add_v6 x y =
let () = assert (x >= 0) in
let rec visit n =
if n = 0
then y
else let n' = n - 1
in let ih = visit n'
in succ ih
in visit x;;
Modulo the name of the formal parameter of visit, the result coincides with the definition of add_v0 in Week 05 (Exercise 08), and so we do fall back on our feet.
N.B.: For each of the successive definitions, we use the unit tests as regression tests.
Pablito: Ahem. I notice that you guys picked my shorter generic definition of add.
Mimer: That is correct, Pablito, and thanks again for it. Would it have been a problem to pick the longer one that uses (fun ih -> succ ih) instead of succ?
Pablito: I guess not – there would have been one more step to apply (fun ih -> succ ih) to ih, that’s all.
Mimer: Yup.
We had generically defined mul as:
let mul_v5 x y =
nat_fold_right 0 (fun ih -> ih + y) x;;
Let us unfold the call to nat_fold_right, i.e., inline nat_fold_right:
let mul_v6 x y =
let n = x
and succ_case = (fun ih -> ih + y)
and zero_case = 0
in let () = assert (n >= 0) in
let rec visit n =
if n = 0
then zero_case
else let n' = n - 1
in let ih = visit n'
in succ_case ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let mul_v7 x y =
let () = assert (x >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in (fun ih -> ih + y) ih
in visit x;;
Applying (fun ih -> ih + y) yields:
let mul_v8 x y =
let () = assert (x >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in let ih = ih
in ih + y
in visit x;;
The inner declaration of ih is the identity declaration, so we can unfold this let expression:
let mul_v9 x y =
let () = assert (x >= 0) in
let rec visit n =
if n = 0
then 0
else let n' = n - 1
in let ih = visit n'
in ih + y
in visit x;;
Modulo the name of the formal parameter of visit and the call to + instead of to add_v0, the result coincides with the definition of mul_v0 in Week 06 (Exercise 10), and so we do fall back on our feet.
N.B.: For each of the successive definitions, we use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 04 in Week 06, inline nat_fold_right in your solution, and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
We had generically defined evenp as:
let evenp_v2 n =
nat_fold_right true not n;;
Let us inline the call to nat_fold_right:
let evenp_v7 x =
let n = x
and succ_case = not
and zero_case = true
in let () = assert (n >= 0) in
let rec visit n =
if n = 0
then zero_case
else let n' = n - 1
in let ih = visit n'
in succ_case ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let evenp_v8 x =
let () = assert (x >= 0) in
let rec visit n =
if n = 0
then true
else let n' = n - 1
in let ih = visit n'
in not ih
in visit x;;
Modulo the name of the formal parameter of visit, the result coincides with the definition of evenp_v0 in Week 05 (Section The even predicate), and so we do fall back on our feet.
N.B.: For each of the successive definitions, we use the unit tests as regression tests.
Along the lines of the previous section, revisit Exercise 05 in Week 06, inline nat_fold_right in your solution, and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit fac_v2 in Section The case of the Factorial numbers, inline nat_parafold_right in this definition, and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 25 in Week 06, inline nat_fold_right in your definition, and discover its recursion pattern.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 15 in Week 06, inline whichever of nat_fold_right or nat_parafold_right you used in your generic definition, and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 17 in Week 06, inline whichever of nat_fold_right or nat_parafold_right you used in your generic definition, and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 08 in Week 06, inline nat_parafold_right in your generic definition of nat_fold_right and verify that you fall back on your feet.
Remember to use the unit tests as regression tests.
Along the lines of the previous sections, revisit Exercise 26 in Week 06, inline nat_fold_right in your generic definition of nat_parafold_right, and discover its recursion pattern.
Remember to use the unit tests as regression tests.
Created [18 Sep 2022]