I'd like to emphasize that there is a precedent to non-recursive let in the world of (relatively pure) lazy functional programming. The programming language Clean has such non-recursive let and uses it and the shadowing extensively. They consider shadowing a virtue, for uniquely typed data. Richard A. O'Keefe wrote
let (x,s) = foo 1 [] in let (y,s) = bar x s in let (z,s) = baz x y s in ...
I really wish you wouldn't do that. ... I find that that when the same name gets reused like that I get very confused indeed about which one I am looking at right now. ... If each instance of the variable is labelled with a sequence number, I don't get confused because each variable has a different name and I can *see* which one this is.
Yes, sequence numbering variable states is a chore for the person writing the code, but it's a boon for the person reading the code.
Let me point out the latest Report on the programming language Clean http://clean.cs.ru.nl/download/doc/CleanLangRep.2.2.pdf specifically PDF pages 38-40 (Sec 3.5.4 Let-Before Expression). Let me quote the relevant part: Many of the functions for input and output in the CLEAN I/O library are state transition functions. Such a state is often passed from one function to another in a single threaded way (see Chapter 9) to force a specific order of evaluation. This is certainly the case when the state is of unique type. The threading parameter has to be renamed to distinguish its different versions. The following example shows a typical example: Use of state transition functions. The uniquely typed state file is passed from one function to another involving a number of renamings: file, file1, file2) readchars:: *File -> ([Char], *File) readchars file | not ok = ([],file1) | otherwise = ([char:chars], file2) where (ok,char,file1) = freadc file (chars,file2) = readchars file1 This explicit renaming of threaded parameters not only looks very ugly, these kind of definitions are sometimes also hard to read as well (in which order do things happen? which state is passed in which situation?). We have to admit: an imperative style of programming is much easier to read when things have to happen in a certain order such as is the case when doing I/O. That is why we have introduced let-before expressions. It seems the designers of Clean have the opposite view on the explicit renaming (that is, sequential numbering of unique variables). Let-before expressions have a special scope rule to obtain an imperative programming look. The variables in the left- hand side of these definitions do not appear in the scope of the right-hand side of that definition, but they do appear in the scope of the other definitions that follow (including the root expression, excluding local definitions in where blocks. Notice that a variable defined in a let-before expression cannot be used in a where expression. The reverse is true however: definitions in the where expression can be used in the let before expression. Use of let before expressions, short notation, re-using names taking use of the special scope of the let before) readchars:: *File -> ([Char], *File) readchars file # (ok,char,file) = freadc file | not ok = ([],file) # (chars,file) = readchars file = ([char:chars], file) The code uses the same name 'file' all throughout, shadowing it appropriately. Clean programmers truly do all IO in this style, see the examples in http://clean.cs.ru.nl/download/supported/ObjectIO.1.2/doc/tutorial.pdf [To be sure I do not advocate using Clean notation '#' for non-recursive let in Haskell. Clean is well-known for its somewhat Spartan notation.] State monad is frequently mentioned as an alternative. But monads are a poor alternative to uniqueness typing. Granted, if a function has one unique argument, e.g., World, then it is equivalent to the ST (or IO) monad. However, a function may have several unique arguments. For example, Arrays in Clean are uniquely typed so they can be updated destructively. A function may have several argument arrays. Operations on one array have to be serialized (which is what uniqueness typing accomplishes) but the relative order among operations on distinct arrays may be left unspecified, for the compiler to determine. Monads, typical of imperative programs, overspecify the order. For example, do x <- readSTRef ref1 y <- readSTRef ref2 writeSTRef ref2 (x+y) the write to ref2 must happen after reading ref2, but ref1 could be read either before or after ref2. (Assuming ref2 and ref1 are distinct -- the uniqueness typing will make sure of it.) Alas, in a monad we cannot leave the order of reading ref1 and ref2 unspecified. We must choose the order, even if it is irrelevant. Overspecification inhibits the possible optimizations. Why Clean is relatively unknown? Well, why is Amiga?