Given an expression e1 of type unit and an expression e2 of type t, the compound expression, which has type t:
let () = e1
in e2
is syntactically sugared into the sequence expression, which also has type t:
e1; e2
Evaluating either expression requires first evaluating e1. If this evaluation completes, it yields a value of type unit. Evaluating either expression then reduces to evaluating e2.
| SEQ | G |- e1 : unit | G |- e2 : t | |
| G |- e1; e2 : t | |||
In words: in any type environment G, the expression e1; e2 has type t whenever in that environment, e1 has type unit and e2 has type t.
For example, the following two expressions have the type int:
let () = Printf.printf "Hello world!\n" in 33 (* <-- implicit sequencing *)
Printf.printf "Hello world!\n"; 33 (* <-- explicit sequencing *)
Evaluating either of them
To wit:
# let () = Printf.printf "Hello world!\n" in 33;; (* <-- implicit sequencing *)
Hello world!
- : int = 33
# Printf.printf "Hello world!\n"; 33;; (* <-- explicit sequencing *)
Hello world!
- : int = 33
#
The printf-expression is evaluated for its effect, since its result is not significant.
These two expressions mean the same (e.g., they are compiled to the same object code). The short hand ; for sequencing is more convenient in practice.
For a last example, here is again the example of the previous lecture note about references:
let r = ref 1 (* <-- creation of a reference *)
in let x = !r (* <-- dereference *)
in let () = r := 10 in (* <-- mutation of the reference and implicit sequencing *)
let y = !r (* <-- dereference *)
in x + y;;
This example can be equivalently written using the short-hand notation for sequencing:
let r = ref 1 (* <-- creation of a reference *)
in let x = !r (* <-- dereference *)
in r := 10; (* <-- mutation of the reference and explicit sequencing *)
let y = !r (* <-- dereference *)
in x + y;;
Likewise, functions that emit traces can be written using the short-hand notation for sequencing Printf.printf ...; blah instead of the long-hand notation let () = Printf.printf ... in blah.
So every time we want to restrict a function to only operate on non-negative number and write:
let fac n_given =
let () = assert (n_given >= 0) in (* <-- implicit sequencing *)
let rec visit n =
if n = 0
then 1
else n * visit (pred n)
in visit n_given;;
we can write:
let fac n_given =
assert (n_given >= 0); (* <-- explicit sequencing *)
let rec visit n =
if n = 0
then 1
else n * visit (pred n)
in visit n_given;;
Ditto for tracing functions. Rather than writing:
let traced_fac n =
let rec visit n i =
let () = Printf.printf "%svisit %s ->\n" (indent i) (show_int n) in (* <-- implicit sequencing *)
let result = (if n = 0
then 1
else n * (visit (pred n) (succ i)))
in let () = Printf.printf "%svisit %s <- %s\n" (indent i) (show_int n) (show_int result) in (* <-- implicit sequencing *)
result
in visit n 0;;
we can write:
let traced_fac' n =
let rec visit n i =
Printf.printf "%svisit %s ->\n" (indent i) (show_int n); (* <-- explicit sequencing *)
let result = (if n = 0
then 1
else n * (visit (pred n) (succ i)))
in Printf.printf "%svisit %s <- %s\n" (indent i) (show_int n) (show_int result); (* <-- explicit sequencing *)
result
in visit n 0;;
And ditto for The imperative simulation of String.mapi in terms of String.map. Rather than writing:
let string_mapi f s =
let i = ref ~-1
in String.map (fun c ->
let () = i := succ !i in (* <-- implicit sequencing *)
f !i c)
s
we can write:
let string_mapi f s =
let i = ref ~-1
in String.map (fun c ->
i := succ !i; (* <-- explicit sequencing *)
f !i c)
s
Is sequencing associative?
For any expressions e1, e2, and e3,
evaluating e1; (e2; e3) proceeds as evaluating let () = e1 in (let () = e2 in e3), i.e., let () = e1 in let () = e2 in e3, which requires first evaluating e1; if this evaluation completes, it yields the unit value and evaluating e1; (e2; e3) reduces to evaluating (e2; e3), i.e., e2; e3;
evaluating e2; e3, i.e., let () = e2 in e3 requires first evaluating e2; if this evaluation completes, it yields the unit value and evaluating e2; e3 reduces to evaluating e3;
evaluating (e1; e2); e3 proceeds as evaluating let () = let () = e1 in e2 in e3, which requires first evaluating e1; e2, i.e., let () = e1 in e2;
evaluating e1; e2 requires first evaluating e1; if this evaluation completes, it yields the unit value and evaluating e1; e2 reduces to evaluating e2;
if evaluating e2 completes, it yields the unit value and evaluating (e1; e2); e3 reduces to evaluating e3.
To sum up, in both cases,
in that order. So if computational effects take place (from tracing to raising an error to diverging), they do in the same order. If the two first evaluations complete, they give rise to the unit value, and evaluating either expression reduces to evaluating e3.
Therefore yes, the expressions e1; (e2; e3) and (e1; e2); e3 are observationally equivalent: sequencing is associative in OCaml.
So for example:
# Printf.printf "hello"; (Printf.printf " "; (Printf.printf "world\n"; 33));;
hello world
- : int = 33
# ((Printf.printf "hello"; Printf.printf " "); Printf.printf "world\n"); 33;;
hello world
- : int = 33
#
In practice, just like for addition and multiplication, the parentheses are redundant and so they are omitted:
# Printf.printf "hello"; Printf.printf " "; Printf.printf "world\n"; 33;;
hello world
- : int = 33
#
Is sequencing commutative?
Alfrothul: No it isn’t in general.
Harald: Well, right. If something happens, and then something else, most of the time the result is not the same as vice versa.
Vigfus: But if I turn left, and then right, or right, and then left, I do get to the same place in a taxicab geometry.
Harald: True enough, but we are talking sequencing in programming, where side effects can take place.
Alfrothul: For example, incrementing a variable by 1 and then multiplying it by 2 doesn’t give the same result as multiplying it by 2 and then incrementing it by 1.
Vigfus: But that’s because the functions fun x -> 2 * (x + 1) and fun x -> (2 * x) + 1 are not equivalent.
Harald: Right. But the issue here is imperative. Look:
# let x = ref 1 and y = ref 10 in x := !x + !y; y := !x + !y; (!x, !y);;
- : int * int = (11, 21)
# let x = ref 1 and y = ref 10 in y := !x + !y; x := !x + !y; (!x, !y);;
- : int * int = (12, 11)
#
Vigfus: Ah, your point is that the two expressions x := !x + !y; y := !x + !y and y := !x + !y; x := !x + !y are not observationally equivalent.
Harald: Precisely, since each occurrence of !x + !y accesses both references in reading, and each assignment accesses one of these references in writing.
Alfrothul: Sequentializing computations in the presence of side effects is not easy at all.
Vigfus: You said that sequencing is not commutative in general?
Alfrothul: Well, yes, that was the point of the example just above.
Vigfus: Are there examples where sequencing is commutative?
Alfrothul: Actually yes, when the effects (read or write) are independent of each other. Look:
# let x = ref 1 and y = ref 10 in x := !x + 1; y := !y + 1; (!x, !y);;
- : int * int = (2, 11)
# let x = ref 1 and y = ref 10 in y := !y + 1; x := !x + 1; (!x, !y);;
- : int * int = (2, 11)
#
Harald: The commands x := !x + 1 and y := !y + 1 are independent.
Alfrothul: They could be executed in parallel.
The keywords begin and end can be used instead of parentheses to delimit a sequence of OCaml commands, i.e., of expressions of type unit -> unit:
# begin Printf.printf "hello "; Printf.printf "world\n" end;;
hello world
- : unit = ()
#
They make it more patent that what lies in between is a sequence of commands.
With sequence and side effects, we now stand in imperative-programming land, and so instead of simulating, e.g., for-loops, we can use OCaml’s syntactic sugar for them:
The corresponding typing rule reads as follows:
| FORUP | G |- e1 : int | G |- e2 : int | (x : int), G |- e0 : unit | |
| G |- for x = e1 to e2 do e0 done : unit | ||||
| FORDOWN | G |- e1 : int | G |- e2 : int | (x : int), G |- e0 : unit | |
| G |- for x = e1 downto e2 do e0 done : unit | ||||
In words,
Furthermore,
to evaluate for x = e1 to e2 do e0 done,
if n1 > n2, the result of evaluating for x = e1 to e2 do e0 done is the unit value;
otherwise, e0 is evaluated n2 - n1 + 1 times, each of them yielding the unit value, assuming that each evaluation completes:
the result of evaluating for x = e1 downto e2 do e0 done is then the unit value.
to evaluate for x = e1 downto e2 do e0 done,
if n1 < n2, the result of evaluating for x = e1 downto e2 do e0 done is the unit value;
otherwise, e0 is evaluated n1 - n2 + 1 times, each of them yielding the unit value, assuming that each evaluation completes:
the result of evaluating for x = e1 downto e2 do e0 done is then the unit value.
Vocabulary:
Here are four telling examples, where the index of the loop is not used in its body (which is akin to primitive iteration):
# for i = 1 to 3 do Printf.printf "testing\n" done;;
testing
testing
testing
- : unit = ()
# for i = 3 to 1 do Printf.printf "testing\n" done;;
- : unit = ()
# for i = 3 downto 1 do Printf.printf "testing\n" done;;
testing
testing
testing
- : unit = ()
# for i = 1 downto 3 do Printf.printf "testing\n" done;;
- : unit = ()
#
Vigfus (reflectively): Wow. Exercise 1 in Week 05 really was salient.
In this interaction,
Here are four more telling examples, where the index of the loop is used in its body (which is akin to primitive recursion):
# for i = 1 to 3 do Printf.printf "testing %d\n" i done;;
testing 1
testing 2
testing 3
- : unit = ()
# for i = 3 to 1 do Printf.printf "testing %d\n" i done;;
- : unit = ()
# for i = 3 downto 1 do Printf.printf "testing %d\n" i done;;
testing 3
testing 2
testing 1
- : unit = ()
# for i = 1 downto 3 do Printf.printf "testing %d\n" i done;;
- : unit = ()
#
In this interaction,
To implement for-loops in OCaml, we Church-encode the index, i.e., we make it an argument of a function whose body is the body of the for-loop:
let up_for i j f =
if i > j
then ()
else let rec loop n =
if n = j
then f n
else begin
f n;
loop (succ n)
end
in loop i;;
let down_for i j f =
if i < j
then ()
else let rec loop n =
if n = j
then f n
else begin
f n;
loop (pred n)
end
in loop i;;
To wit, let us revisit the first batch of examples, where the index of the for-loop is not used in the body of the loop:
# up_for 1 3 (fun i -> Printf.printf "testing\n");;
testing
testing
testing
- : unit = ()
# up_for 3 1 (fun i -> Printf.printf "testing\n");;
- : unit = ()
# down_for 3 1 (fun i -> Printf.printf "testing\n");;
testing
testing
testing
- : unit = ()
# down_for 1 3 (fun i -> Printf.printf "testing\n");;
- : unit = ()
#
In this interaction,
And likewise, let us revisit the second batch of examples, where the index of the for-loop is used in the body of the loop:
# up_for 1 3 (fun i -> Printf.printf "testing %d\n" i);;
testing 1
testing 2
testing 3
- : unit = ()
# up_for 3 1 (fun i -> Printf.printf "testing %d\n" i);;
- : unit = ()
# down_for 3 1 (fun i -> Printf.printf "testing %d\n" i);;
testing 3
testing 2
testing 1
- : unit = ()
# down_for 1 3 (fun i -> Printf.printf "testing %d\n" i);;
- : unit = ()
#
The implementation of up_for and down_for are properly tail-recursive in that the last iteration is implemented with a tail call. Let us illustrate this point first with up_for and then with down_for:
# let rec test () = for i = 1 to 1 do test () done in test ();;
Stack overflow during evaluation (looping recursion?).
# let rec test () = up_for 1 1 (fun i -> test ()) in test ();;
Dines Bjørner: As part of this job interview, could you write a program that loops twice in a row?Loki: Certainly.Mimer: Prof. Bjørner! Thanks for looping by!Dines Bjørner (modestly): Just the once, just the once.
Implement an OCaml function that maps a given string to the corresponding list of characters:
let test_chars_of_string candidate =
let b0 = (candidate "" = [])
and b1 = (candidate "0" = ['0'])
and b2 = (candidate "01" = ['0'; '1'])
and b3 = (candidate "012" = ['0'; '1'; '2'])
and b4 = (candidate "abcd" = ['a'; 'b'; 'c'; 'd'])
in b0 && b1 && b2 && b3 && b4;;
The following implementation traverses the string from right to left, starting from the empty list and accumulating one character onto another to construct the resulting list:
let fun_chars_of_strings s =
let rec loop n a =
if n = 0
then a
else let n' = pred n
in loop n' (s.[n'] :: a)
in loop (String.length s) [];;
This implementation is a fit for nat_parafold_left:
let nat_parafold_left zero_case succ_case n =
let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else let i' = pred i
in loop i' (succ_case i a)
in loop n zero_case;;
let fun_chars_of_strings_alt s =
nat_parafold_left
[]
(fun i a ->
s.[i] :: a)
(String.length s);;
In the functional solution just above, loop has type int -> char list -> char list: it “threads” the accumulator in that given one, it returns a new one. (Technically, applying loop to an integer yields an endofunction: a function whose domain is also its co-domain. Here this function is an accumulator transformer.) Imagine that we want loop to have type int -> unit and do the same job. The accumulator would then need to become implicit:
The accumulator would then be referred to in the lexical environment of loop, and this reference would be mutable. Concretely:
let imp_chars_of_strings s =
let a = ref []
in let rec loop n =
if n = 0
then ()
else let n' = pred n
in begin
a := s.[n'] :: !a;
loop n'
end
in begin
loop (String.length s);
!a
end;;
This solution can be made “for-ready”, by making loop iterate from the last index of the given string down to its first and stop when the index becomes out of bounds:
let massaged_imp_chars_of_strings s =
let a = ref []
in begin
let rec loop n =
if n < 0
then ()
else begin
a := s.[n] :: !a;
loop (pred n)
end
in loop (String.length s - 1);
!a
end;;
This massaged version can be syntactically sugared with a for-loop, as in the following alternative solution.
The following implementation traverses the string from right to left, accumulating one character onto another to construct the resulting list. To this end, a for-loop with decreasing indices is used. Its body side-effects a reference that holds the list under construction:
let for_chars_of_strings s =
let a = ref []
in begin
for n = String.length s - 1 downto 0 do
a := s.[n] :: !a
done;
!a
end;;
Re-implement up_for using nat_parafold_right and then using nat_parafold_left. The following unit tests should be satisfied:
# up_for_pararight 1 3 (fun i -> Printf.printf "%d\n" i);;
1
2
3
- : unit = ()
# up_for_pararight 3 1 (fun i -> Printf.printf "%d\n" i);;
- : unit = ()
# up_for_paraleft 1 3 (fun i -> Printf.printf "%d\n" i);;
1
2
3
- : unit = ()
# up_for_paraleft 3 1 (fun i -> Printf.printf "%d\n" i);;
- : unit = ()
#
Subsidiary questions:
Re-implement down_for using nat_parafold_right and then using nat_parafold_left. The following unit tests should be satisfied:
# down_for_pararight 3 1 (fun i -> Printf.printf "%d\n" i);;
3
2
1
- : unit = ()
# down_for_pararight 1 3 (fun i -> Printf.printf "%d\n" i);;
- : unit = ()
# down_for_paraleft 3 1 (fun i -> Printf.printf "%d\n" i);;
3
2
1
- : unit = ()
# down_for_paraleft 1 3 (fun i -> Printf.printf "%d\n" i);;
- : unit = ()
#
Subsidiary questions:
In the particular case where the body of the for-loop does not use the index of the loop, re-implement up_for using nat_fold_right and then using nat_fold_left. The following unit tests should be satisfied:
# up_for_right 1 3 (fun () -> Printf.printf "hello\n");;
hello
hello
hello
- : unit = ()
# up_for_right 3 1 (fun () -> Printf.printf "hello\n");;
- : unit = ()
# up_for_left 1 3 (fun () -> Printf.printf "hello\n");;
hello
hello
hello
- : unit = ()
# up_for_left 3 1 (fun () -> Printf.printf "hello\n");;
- : unit = ()
#
Subsidiary questions:
In the particular case where the body of the for-loop does not use the index of the loop, re-implement down_for using nat_fold_right and then nat_fold_left. The following unit tests should be satisfied:
# down_for_right 3 1 (fun () -> Printf.printf "hello\n");;
3
2
1
- : unit = ()
# down_for_right 1 3 (fun () -> Printf.printf "hello\n");;
- : unit = ()
# down_for_left 3 1 (fun () -> Printf.printf "hello\n");;
3
2
1
- : unit = ()
# down_for_left 1 3 (fun () -> Printf.printf "hello\n");;
- : unit = ()
#
Subsidiary questions:
In the light of Exercice 3, Exercice 4, Exercice 5, and Exercice 6, what can be concluded about the relation between for-loops that use their index, for-loops that do not use their index, primitive iteration (i.e., nat-fold functions), and primitive recursion (i.e., nat-parafold functions)?
It is generally a good idea to repeat tests over random input. To this end, implement a repeat loop as an OCaml function of type int -> (unit -> unit) -> unit that is such that:
Be imaginative: provide implementations that use for-loops and others that are (tail-)recursive. Also, the more pilfering in the up_for and down_for menagerie, the better.
As per what is mentioned just before Exercise 2, are your implementations properly tail recursive?
As stated above, with sequence and side effects, we now stand in imperative-programming land, and so instead of simulating, e.g., while-loops, we can use OCaml’s syntactic sugar for them:
The corresponding typing rule reads as follows:
| WHILE | G |- e1 : bool | G |- e0 : unit | |
| G |- while e1 do e0 done : unit | |||
In words,
Furthermore,
Vocabulary:
We are now in position to express in OCaml the imperative implementation of the imperative Factorial program in Week 02. To quote:
For a more computational example, imagine a program that works over two memory locations. The first one (call it x) is initialized with 5, and the second (call it a) with 1. The program repeatedly checks whether the content of x is 0, and stops if it is so, with a containing the result. Otherwise, the program multiplies the content of x by the content of a and stores the result at location a, it decrements the content of x, and it iterates.
To code:
let imp_fac n =
let x = ref n and a = ref 1
in begin
while !x <> 0 do
a := !x * !a;
x := pred !x
done;
!a
end;;
To wit:
# imp_fac 5;;
- : int = 120
#
Vigfus: To quote, to code, and to wit.Halcyon: This is so cool!
Implement a mean OCaml function of type (unit -> bool) -> (unit -> unit) -> unit that simulates a while loop so that imp_fac can be expressed as follows:
let imp_fac_alt n =
let x = ref n and a = ref 1
in begin
meanwhile
(fun () ->
!x <> 0)
(fun () ->
begin
a := !x * !a;
x := pred !x
end);
!a
end;;
Can you make your implementation of meanwhile properly tail-recursive, as per what is mentioned just before Exercise 2?
Added a bunch of exercises as well as the resource file [24 Apr 2021]
Added the sections about for-loops and about while-loops [19 Apr 2021]
Fixed two typos in the section about Sequencing in retrospect, thanks to Aditya Singhania’s eagle eye [12 Apr 2021]
Created [03 Apr 2021]