It sounds like you are describing linear types or uniqueness types, not Haskell's monad solution to mutable state. (Haskell supports neither linear nor uniquene

It sounds like you are describing linear types or uniqueness types, not Haskell's monad solution to mutable state. (Haskell supports neither linear nor uniqueness types.) The aerial view of Haskell mutable state is that every function that wants to "really" mutate state secretly takes a "world" parameter and returns a new "world" parameter. Mutable variables are just references to some named "thing" in this world value. It appears to mutate because the thing to which it refers also appears to mutate because the world is being swapped out from underneath it. There is of course only one world value (RAM) and this is really and truly being mutated. Only at the most abstract level can this be considered immutable, but there are still theoretical advantages to operating at this level, e.g., there is an implementation of the IO monad (IOSpec I think?) that truly does keep a copy of the world around, which is useful for testing and such. The main difference is that Haskell maintains uniqueness of only one secret paramter, the world, while linear or uniqueness types can do it on a per-value basis (which sounds to me like what you described.) The bad news is that this is much less interesting from a theoretical point of view---within the monad side effects are still unconstrained---but from a practical point of view it means imperative programming in haskell is pretty accessible, funny vocabulary notwithstanding.