[PL-sem-jr] answer to my ML question

[Dave Herman]

Xavier Leroy gives an explanation of SML's restriction:

http://groups.google.com/group/comp.lang.ml/tree/browse_frm/thread/e1e2bbb9cb25591c/83164e48fa60c535#doc_266106904b3d3708

The short story: it's actually sound to relax the "val rec" restriction 
to allow the rhs to include syntactic functions, variable references, 
constants, and constructor applications, since none of these have side 
effects. However, at least back in the day, it was considered very hard 
to prove this sound. (My guess: this was before the popularity of 
proving type soundness via operational semantics.) Apparently OCaml 
relaxes the restriction, but SML is stuck in the dark ages. :(

Dave