Should the state of the ST not change in order to be executed by the runST?

Question

type ST s a = ST (s -> (s, a))

runST :: (forall s. ST s a) -> a
runST (ST f) = case (f realWorld) of (_, a) -> a

If you look closely, there are many errors, but the overall structure of runST is as above.

So, if you want to apply runST to a value of type ST s a, which is identical to s -> (s, a), its type s must be fully parameterized.

Some kinds of functions depending on concrete type can't applied by runST. Example of inappropriate function is below.

\s -> (s + s, "hello world")   // this won't run cause it depends on (Num) type class.

fun [] = ([], 0)
fun (x : xs) = (xs, length (x : xs))  // this won't run. It depends on ([]) type.

So, functions to be executed by runST should be as follows.

\s -> (s, fun s)

fun = maybe some native code, not haskell.

The point is that s from (s, a) term of s -> (s, a) should always same as s itself, like an identity.

We call it parametricity.

Currently I know that if s has RealWorld in it, even what seems to be an id can make meaningful calculations. (Although it's not pure Haskell).

To prove what I guessed, I prepared the following experiment.

//given
newMutVar# :: v -> State# s -> (# State# s, MutVar# s v #)

//then (this is pseudo code)
let (# s#, var# #) = newMutVar# "hello world" (State# 0) in
    s# == State# 0

and see if the result is True, which implies that newMutVar# acts like id for State#.

But I can't do this because I don't know how to generate State# s value. I know how to do it only for RealWorld, and its meaningless cause RealWorld only has one value inside so it always be identical no matter what the mapping is.

Also, even if I succeed generating State# 0, there's no way to compare State# 0 to s#, cause State# s doesn't implement Eq.

Answer 1

I think you've conflated the State type with ST to some extent. I see that you've looked behind the curtains to see how GHC defines ST and IO, but I think you've misinterpreted the meaning of what you see there. You're trying to reason about the implementation as if it was the same thing as State. That's understandable given the use of names like State# and the general structure of definitions like this:

type STRep s a = State# s -> (# State# s, a #)

That sure looks like the idea behind the State type, but that's very misleading. To see why, you need to look at the documentation for State# which ends with a critical sentence: "It is represented by nothing at all."

There is no such thing as a value of type State# Realworld or State# s. A function with a type like STRep s a up there actually is a 0-argument function (the State# s argument is represented by nothing at all) that returns a single value of type a (an unboxed pair of nothing at all and an a value).

This is very magical within the implementation of GHC. You can't create a type like that. (I've discovered that there are enough such types now that GHC actually does expose tools to create your own. But they're far from standard Haskell.) The compiler has recognize it and support all the special cases for handling it correctly. So why bother? Because it serves to bridge the difference in representation between a Haskell function and a machine code procedure. All the optimizations which take place at the Haskell (well, GHC core) level see a regular Haskell function that's doing token passing. The token passing serves to serialize execution so that GHC can't reorder operations when it's doing optimizations. But then when the GHC core is converted into either C-- for the native code gen backend or LLVM IR for the LLVM backend, all the State# values get stripped out so that at a low level you don't have all that useless token passing that the GHC core representation suggested is happening.

So the reason you don't know how to create a State# value is that they don't exist. They're never updated because ST doesn't work anything like State, despite the superficial similarities in their internals.