What is the difference between mutable values and immutable value redefinition?

Question

I have read that values in F# are immutable. However, I have also come across the concept of redefining value definitions, which shadow the previous ones. How is this different from a mutable value ? I ask this not just as a theoretical construct, but also if there is any advice on when to use mutable values and when to redefine expressions instead; or if someone can point out that the latter is not idiomatic f#.

Basic example of redefinition:

let a = 1;;
a;; //1
let a = 2;;
a;; //2

Update 1:

Adding to the answers below, the redefinition in Fsharp interactive at top level is only allowed in different terminations. The following will throw up an error in fsi as well:

let a = 1
let a = 2;;

Error: Duplicate definition of value 'a'

On the other hand, redefinition is allowed in let bindings.

Update 2: Practical difference, closures cannot work with mutable variables:

let f =
   let mutable a = 1
   let g () = a //error
   0  
f;;

Update 3:

While I can model side effects with refs, eg:

let f =
   let  a = ref 1
   let g = a
   a:=2
   let x = !g  + !a
   printfn "x: %i" x //4

f;;

I can't quite see a practical difference between redefinition and using the mutable keyword, besides the difference in usage with closures, eg:

let f  =
   let a = 1
   let g  = a
   let a = 2
   let x = g + a
   printfn "x: %i" x //3

f;;

vs

let f =
   let mutable a = 1
   let g = a
   a <-2
   let x = g  + a
   printfn "x: %i" x //3
 f;;

Another line of thought: I'm not sure how to work with threads, but (a) can another thread can mutate the value of a mutable variable within a let binding and (b) can another thread rebind/redefine a value name within a let binding. I am certainly missing something here.

Update 4: The difference in the last case is that the mutation would still happen from a nested scope, whereas a redefinition/rebinding in the nested scope will 'shadow' definition from the external scope.

let f =
   let mutable a = 1
   let g = a
   if true then
      a <-2   
   let x = g  + a
   printfn "x: %i" x //3

f;;

vs

let f =
   let a = 1
   let g = a
   if true then
      let a = 2  
      printfn "a: %i" a   
   let x = g  + a
   printfn "x: %i" x //2
f;;

Answer 1

'I'm not sure I agree with some of the answers given.

The following compiles and executes perfectly both in FSI and in a real assembly:

let TestShadowing() =
   let a = 1
   let a = 2
   a

But it's important to understand that what is going on is not mutation, but shadowing. In other words the value of 'a' hasn't been reassigned. Another 'a' has been declared with its own immutable value. Why does the distinction matter? Consider what happens when 'a' is shadowed in an inner block:

let TestShadowing2() =
   let a = 1
   printfn "a: %i" a
   if true then
      let a = 2
      printfn "a: %i" a
   printfn "a: %i" a

> TestShadowing2();;
a: 1
a: 2
a: 1

In this case the second 'a' only shadows the first one while the second one is in scope. Once it goes out of scope the first 'a' pops back into existence.

If you don't realize this it can lead to subtle bugs!

Clarification in the light of Guy Coder's comment:

The behaviour I decribe above occurs when the redefinition is within some let binding (i.e. within the TestShadowing() functions in my examples). This I would say is by far the most common scenario in practice. But as Guy says, if you redefine at the top level, e.g.:

module Demo =

   let a = 1
   let a = 2

you will indeed get a compiler error.

Answer 2

I'm not familiar with F# in particular, but I can answer the "theoretical" part.

Mutating an object is (or at least has the potential to be) a globally visible side effect. Any other piece of code with a reference to the same object will observe the change. Any properties that have been established anywhere in the program that were dependent on the value of the object may now be altered. For example, the fact that a list was sorted can be rendered false if you mutate an object that is referenced in that list in a way that affects its sort position. This can be an extremely unobvious and non-local effect - the code dealing with the sorted list and the code doing the mutation may be in completely separate libraries (neither with a direct dependency on the other), connected only through a long chain of calls (some of which may be closures set up by other code). If you're using mutation fairly widely, then there may not even be a direct call-chain link between the two locations, the fact that this mutable object wound up being passed to that mutating code could be dependent on the particular sequence of operations carried out by the program so far.

Rebinding a local variable from one immutable value to another, on the other hand, might still technically be viewed as a "side effect" (depending on the exact semantics of the language), but it's quite a localised one. Because it only has an effect on the name, not on either the before or after value, it doesn't matter where the objects came from or where they'll go to after this. It changes the meaning only of other bits of code that access the name; the places you have to scrutinise for code affected by this is limited to the scope of the name. This is the kind of side effect that is very easy to keep internal to a method/function/whatever, so that the function is still side-effect free (pure; referentially transparent) when viewed from an external perspective - indeed without closures that capture names rather than values I believe it's impossible for this sort of local rebinding to be an externally visible side effect.

Answer 3

This sort of redefinition will only work in fsi. The compiler will produce an error here, although you can occasionally do something like

let f h = match h with h::t -> h

which will return the first element as you create a new h which shadows the definition from the argument.

The only reason that redifintion works is that you might make mistakes in fsi like so

let one = 2;;
let one = 1;; //and fix the mistake

In compiled F# code, this is not possible.

Answer 4

Let me add a more direct answer to the main point of your question, namely, how rebinding differs from mutation. You can observe the difference in this function:

let f () =
   let a = 1
   let g () = a
   let a = 2
   g () + a

which returns 3, since the a in g is referring to the former binding of a, while the latter is separate. The above program is completely equivalent to

let f () =
   let a = 1
   let g () = a
   let b = 2
   g () + b

where I have consistently renamed the second a and all references to it to b.