I've landed to SML pages, comparing call‑by‑name and call‑by‑value, asserting the former always succeed while the latter may fails. As this seems counter intuitive to me, I feel at least an example case would be useful.
Theorem (Church Rosser 1)
For a purely functional language, if call-by-value evaluation and call-by-name evaluation both yield a well-defined result then they yield the same result.
Theorem (Church Rosser 2)
If a well-defined result exists for an expression then the call-by-name evaluation strategy will find it where, in some cases, call-by-value evaluation will not.
What make it counter‑intuitive to me, is that call‑by‑name may re‑evaluate expressions multiple times, which I don't understand how it can make it succeed when call‑by‑value and its one‑time evaluation, would fails. If, as the context is FP and its referential transparency, both expression are supposed to evaluated to the same, how evaluating multiple time may make something succeed or alternatively potentially fails if the same expression is evaluated only once? Unless there are side‑effect somewhere?… is this related to side effects and non‑pure FP?
As a reminder, here is what would look like call‑by‑value and call‑by‑name with SML (if there is an error here, feel free to tell), added call‑by‑need to help not confuse one with the others:
(* This, is supposed to sometime fails… *) fun call_by_value a = a + a (* `a` is evaluated only once *) (* …when this is supposed to succeed *) fun call_by_name a = a () + a () (* `a` is evaluated for each of its reference *) (* None of the above should be confused with call‑by‑need: *) fun call_by_need a = let val a' = a () (* memoization *) in fn () => a' + a' (* to be evaluated when needed *) end val _ = print (Int.toString (call_by_value 2) ^ "\n") val _ = print (Int.toString (call_by_name (fn () => 2)) ^ "\n") val r = call_by_need (fn () => 2) () (* memoization *) val _ = print (Int.toString r ^ "\n")