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 fold_right_nat 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 midterm project.
To verify that we fall back on our feet, we can desugar the instances of fold_right_nat by inlining its definition at its points of call:
let fold_right_nat case_zero case_succ n =
(* fold_right_nat : 'a -> ('a -> 'a) -> int -> 'a *)
let () = assert (0 <= n) in
let rec visit n =
if n = 0
then case_zero
else let n' = n - 1
in let ih = visit n'
in case_succ ih
in visit n;;
We had generically defined twice as:
let twice_v4 n =
fold_right_nat 0 (fun ih -> succ (succ ih)) n;;
Let us inline fold_right_nat, i.e., unfold its call, and conflate the standard two steps of (1) replacing fold_right_nat by its denotation and (2) applying this denotation:
let twice_v5 n =
let case_succ = (fun ih -> succ (succ ih))
and case_zero = 0
and n = n
in let () = assert (0 <= n) in
let rec visit n =
if n = 0
then case_zero
else let n' = n - 1
in let ih = visit n'
in case_succ ih
in visit n;;
The two first clauses of the let expression declare values and they are linear, and the third one renames n to itself, so let us unfold the let expression:
let twice_v6 n =
let () = assert (0 <= n) 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 (0 <= n) 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 (0 <= n) 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 =
fold_right_nat y succ x;;
Let us inline the call to fold_right_nat (again, conflating the standard two steps of replacing fold_right_nat by its denotation and applying this denotation):
let add_v5 x y =
let case_succ = succ
and case_zero = y
and n = x
in let () = assert (0 <= n) in
let rec visit n =
if n = 0
then case_zero
else let n' = n - 1
in let ih = visit n'
in case_succ ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let add_v6 x y =
let () = assert (0 <= x) 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 6), 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.
Vigfus: Ahem. I notice that you guys picked my shorter generic definition of add.
Mimer: That is correct, Vigfus, 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?
Vigfus: I guess not – there would have been one more step to apply (fun ih -> succ ih) to ih, that’s all.
Yod^H^H^HMimer: Right you are.
We had generically defined mul as:
let mul_v5 x y =
fold_right_nat 0 (fun ih -> ih + y) x;;
Let us unfold the call to fold_right_nat, i.e., inline fold_right_nat:
let mul_v6 x y =
let case_succ = (fun ih -> ih + y)
and case_zero = 0
and n = x
in let () = assert (0 <= n) in
let rec visit n =
if n = 0
then case_zero
else let n' = n - 1
in let ih = visit n'
in case_succ ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let mul_v7 x y =
let () = assert (0 <= x) 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 (0 <= x) 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 (0 <= x) 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 7), 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 1 in Week 06, inline fold_right_nat 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 =
fold_right_nat true not n;;
Let us inline the call to fold_right_nat:
let evenp_v7 x =
let case_succ = not
and case_zero = true
and n = x
in let () = assert (0 <= n) in
let rec visit n =
if n = 0
then case_zero
else let n' = n - 1
in let ih = visit n'
in case_succ ih
in visit n;;
The three let expressions declare values, so let us unfold them:
let evenp_v8 x =
let () = assert (0 <= x) 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 2 in Week 06, inline fold_right_nat 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 Exercise 3 in Week 06, inline parafold_right_nat 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 4 in Week 06, inline parafold_right_nat 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 5 in Week 06, inline whichever of fold_right_nat or parafold_right_nat 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 6 in the midterm project, inline parafold_right_nat in your generic definition of fold_right_nat, and verify that you fall back on your feet. Remember to use the unit tests as regression tests.
Adjusted [14 Mar 2020]
Streamlined the unit-test functions [08 Jun 2019]
Fixed a consistent typo in the first derivation, thanks to Yunjeong Lee’s eagle eye [02 May 2019]
Fixed a typo in make_even_number_v1 and make_even_number_v2, thanks to Lukas Fesser’s eagle eye [15 Mar 2019]
Created [05 Mar 2019]