Evaluation order of let-in expressions with tuples

Question

My old notes on ML say that

let (₁, … , ₙ) = (₁, … , ₙ) in ′

is a syntactic sugar for

(λ ₙ. … (λ ₁. ′)₁ … )ₙ

and that

let (₁, ₂) =  ′ in ″

is equivalent to

let  =  ′ in 
let ₂ = snd  in 
let ₁ = fst  in 
″

where

• each (with or without a subscript) stands for a variable,
• each (with or without a sub- or a superscript) stands for a term, and
• fst and snd deliver the first and second component of a pair, respectively.

I'm wondering whether I got the evaluation order right because I didn't note the original reference. Could anyone ((confirm or reject) and (supply a reference))?

Answer 1

It shouldn't matter whether it's:

let  =  ′ in 
let ₂ = snd  in 
let ₁ = fst  in 
″

Or:

let  =  ′ in  
let ₁ = fst  in
let ₂ = snd  in 
″

Since neither fst nor snd have any side-effects. Side-effects may exist in the evaluation of ′ but that's done before the let binding takes place.

Additionally, as in:

let (₁, ₂) =  ′ in ″

Neither ₁ nor ₂ is reliant on the value bound to the other to determine its value, so the order in which they're bound is again seemingly irrelevant.

All of that said, there may be an authoritative answer from those with deeper knowledge of the SML standard or the inner workings of OCaml's implementation. I simply am uncertain of how knowing it will provide any practical benefit.

Practical test

As a practical test, running some code where we bind a tuple of multiple expressions with side-effects to observe order of evaluation. In OCaml (5.0.0) the order of evaluation is observed to be right-to-left. We observe tthe same when it comes to evaluating the contents of a list where those expressions have side-effects as well.

# let f () = print_endline "f"; 1 in
let g () = print_endline "g"; 2 in
let h () = print_endline "h"; 3 in
let (a, b, c) = (f (), g (), h ()) in a + b + c;;
h
g
f
- : int = 6
# let f () = print_endline "f"; 1 in
let g () = print_endline "g"; 2 in
let h () = print_endline "h"; 3 in
let (c, b, a) = (h (), g(), f ()) in a + b + c;;
f
g
h
- : int = 6
# let f _ = print_endline "f"; 1 in
let g () = print_endline "g"; 2 in
let h () = print_endline "h"; 3 in
let a () = print_endline "a" in
let b () = print_endline "b" in
let (c, d, e) = (f [a (); b ()], g (), h ()) in
c + d + e;;
h
g
b
a
f
- : int = 6

In SML (SML/NJ v110.99.3) we observe the opposite: left-to-right evaluation of expressions.

- let
=   fun f() = (print "f\n"; 1)
=   fun g() = (print "g\n"; 2)
=   fun h() = (print "h\n"; 3)
=   val (a, b, c) = (f(), g(), h())
= in
=  a + b + c
= end;
f
g
h
val it = 6 : int
- let
=   fun f() = (print "f\n"; 1)
=   fun g() = (print "g\n"; 2)
=   fun h() = (print "h\n"; 3)
=   val (c, b, a) = (h(), g(), f())
= in
=   a + b + c
= end;
h
g
f
val it = 6 : int
- let
=   fun f _ = (print "f\n"; 1)
=   fun g() = (print "g\n"; 2)
=   fun h() = (print "h\n"; 3)
=   fun a() = print "a\n"
=   fun b() = print "b\n"
=   val (c, d, e) = (f [a(), b()], g(), h())
= in
=   c + d + e
= end;
a
b
f
g
h
val it = 6 : int

Answer 2

Be aware that, in OCaml, due to the (relaxation of the) value restriction, let a = b in c is not equivalent to (fun a -> c)b. A counterexample is

# let id = fun x -> x in id 5, id 'a';;
- : int * char = (5, 'a')
# (fun id -> id 5, id 'a')(fun x -> x)
Error: This expression has type char but an expression was expected of type int
#

This means that they are semantically not the same construction (the let ... = ... in ... is strictly more general that the other).

This happens because, in general, the type system of OCaml doesn't allow types of the form (∀α.α→α) → int * char (because allowing them would make typing undecidable, which is not very practical), which would be the type of fun id -> id 5, id 'a'. Instead, it resorts to having the less general type ∀α.(α→α) → α * α, which doesn't make it typecheck, because you can't unify both α with char and with int.