If this is always possible without cheating, then I have definitely misunderstood something about Haskell.
Could you point me towards an explanation how the hiding of stateful expressions works in Haskell in general?
Let me clarify my question (a bit). Are you saying one of the following is true?
(1) You are saying for any program M that uses state (i.e. M's type mentions the state monad in an essential way) but in a pure way, i.e. M's stateful behaviour is not visible from the outside, there is a context C[.] (not involving tricks like UnsafeIO) such that C[M] has the same behaviour as M (as seen from the outside), and C[M] has (essentially) the same type as M, except that the state monad is gone?
(2) There is a 'nice' translation function f on programs such that for any
program M that uses state in a pure way (same as (1)), f(M) has the same behaviour as M (as
seen from the outside), and f(M) has (essentially) the same type as
M, except that the state monad is gone?
I'm not sure I understand the distinction (quite possibly just 'cause it's early).
A fruitful way to look at monads is to say a value of type M (where M is an instance of Monad) is a program in a language. State is a language for describing stateful computation. Reader is a language for describing parameterized computation. ST is a language for describing controlled, local mutation. IO is a language for describing arbitrary side effects.
Most of these have pure interpreters, with the most generic typically called runM (so, runState, runReader, &c). The only place cheating comes in is unsafePerformIO - interpreting IO is the job of the runtime, which does it in a more controlled way relative to the rest of your program.
The type of the return value of an interpreter, of course, doesn't tell you what kind of program you ran - it just tells you the result.
Revisiting to speak directly to the question you've asked, both 1 and 2 are true for the State monad.
For 1, to get from a value of type "State s a" to a value of type a, you simply call evalState and supply an initial state of type s.
For 2, you could look at the structure of the program and unwrap all (State s a) values to have type (s -> (a, s)), updating the various functions used to operate on (State s a) values to match.
In either case, you would not see State in the resulting type signature. In case 2, you would still need to provide an initial value of type s - you can't do much interesting with a function but apply it.
Note that the function in 2 is more theoretical than practical. You could in principle write it with Template Haskell, but since it doesn't change the behavior and you can just do 1 to change the type the same way there isn't reason to.
Thanks. This is very interesting, but different from what I used to believe about Haskell (as you can imagine, I'm not an active Haskell programmer). I will have to revisit my ideas.
I still wonder how this would work with scope extrusion of references. Consider this little Ocaml program
let ( impure, pure ) =
let i = ref 0 in
let impure x = ( i := !i + 1; x + !i ) in
let pure x = (
i := !i + 1;
let res = !i + x in
i := !i - 1;
res - !i ) in
( impure, pure );;
which returns two functions called "pure" and "impure". Both are of type int -> int. The function "pure" is computing the successor function (let's ignore corner cases), but using hidden state. The function "impure" is using the same hidden state, but is clearly impure.
Is it possible to do the same in Haskell? By "the same" I mean giving "pure" the type int -> int, despite using hidden state that is used elsewhere?
It's harder to be confident about impossibility than about possibility, but I think this would require "cheating". I'm not sure if you meant it as a bug, but note that outside of a single-threaded context "pure" isn't referentially transparent - there seems to be a race condition that could lead to pure computing different values if impure is called during pure's execution.
Something with a similar form that would be more realistic to ask for would be a cache for a pure-but-expensive function and some IO operations to inspect/manipulate that cache. I believe you would need a call to unsafePerformIO, but that could be a reasonable thing to do.
Thanks. I know that "pure" is not thread-safe. I'm quite happy to consider the expressivity of Haskell's monadic approach to effects in a sequential setting first -- much easier to reason about. I wonder if anybody has investigated this expressivity problem. If not, there's an interesting problem waiting to be tackled.
I don't see the problem. Pure code being automatically thread-safe is a boon. I would much rather be unable to write thread-unsafe code without noticing (and able to when I deliberately decide to).
My interest is in proving expressivity results. Such proofs are much easier in a sequential setting. Indeed, at this point I don't even have a strong intuition what exactly the expressivity limitations of Haskell's monadic effect control are.
Could you point me towards an explanation how the hiding of stateful expressions works in Haskell in general?
Let me clarify my question (a bit). Are you saying one of the following is true?
(1) You are saying for any program M that uses state (i.e. M's type mentions the state monad in an essential way) but in a pure way, i.e. M's stateful behaviour is not visible from the outside, there is a context C[.] (not involving tricks like UnsafeIO) such that C[M] has the same behaviour as M (as seen from the outside), and C[M] has (essentially) the same type as M, except that the state monad is gone?
(2) There is a 'nice' translation function f on programs such that for any program M that uses state in a pure way (same as (1)), f(M) has the same behaviour as M (as seen from the outside), and f(M) has (essentially) the same type as M, except that the state monad is gone?