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 =
let () = assert (n >= 0) in (* <-- implicit sequencing *)
let rec visit n =
if n = 0
then 1
else n * visit (pred n)
in visit n_init;;
we can write:
let fac n =
assert (n >= 0); (* <-- explicit sequencing *)
let rec visit n =
if n = 0
then 1
else n * visit (pred n)
in visit n_init;;
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.
Added the solution for Exercise 1 [05 Apr 2020]
Added an example to the section about Sequencing in retrospect [05 Apr 2020]
Created [24 Mar 2020]