Le mar. 3 nov. 2015 à 13:24, PATRICK BROWNE <patrick.browne@dit.ie> a écrit :

Chaddaï,
Thank you very much for your response to my question. It confirms my intuition, but I was not sure.

Is it true in general that let expressions (e.g. eligibleLet) are always semantically equivalent to their equational  counterparts (e.g. eligibleEquational)?


Yes, in Haskell that is true because it is pure/referentially transparent (absent case of misuse of the "escape hatch"es like unsafePerformIO). That is one of the big advantage : that you're always able to reason equationally. (note that this remains true with monads, they're not impure, they're just a notation that can describe impure computations)
 

Would it be fair to say that "let" is syntactic sugar for an equational equivalent? Or is there more to it?


"let x = stuff in expr" is syntactic sugar for "(\x -> expr) stuff" basically. Though there's a few syntactical conveniences that complicate the translation.
 
With respect to the ordering of the operations is generally true that a monadic version is semantically equivalent to a set of "let expressions"  in a nested if-then-else?

Well with the Maybe monad like here yes, though that's more of a nested case-of. With IO this is more complicated, especially if you use forkIO (concurrency).
 

Thanks,

You're welcome !
--
Chaddaï