How to understand the state type in Haskell's

Question

Jones and Launchbury described in their paper "Lazy Functional State Threads" the ST monad. To ensure that mutable variables can't be used outside the context (or "thread") they have been created in, they use special types, including one of higher rank. Here four important examples:

newVar   :: ∀ s a. a -> ST s (MutVar s a)
readVar  :: ∀ s a. MutVar s a -> ST s a
writeVar :: ∀ s a. MutVar s a -> a -> ST s ()
runST    :: ∀   a. (∀ s. ST s a) -> a

In order to get the idea behind that construction I read the first two sections of the paper. The following explanation seems to be central:

Now, what we really want to say is that newST should only be applied to a state transformer which uses newVar to create any references which are used in that thread. To put it another way, the argument of runST should not make any assumptions about what has already been allocated in the initial state. That is, runST should work regardless of what initial state it is given. So the type of runST should be: runST :: ∀ a. (∀ s. ST s a) -> a

The explanation is fine, but I wonder how it maps to the final definition of the required type. My problem is that I don't know how to interpret the type variable s. As stated in Section 1, a state is essentially a mapping from variables to values. But what is a state type s? In what can a state type s differ from another one t? For me there are two possibilities:

(1) The type s can be seen as the concrete type for a mapping of variables such as lists, arrays and sequences can be seen as concrete types for sequential collections. (I intentionally avoid here the words "class" and "implementation" as there is no class restriction on the type of s.)

(2) The type s can be seen as a concrete value, i.e. a concrete state, i.e. a concrete mapping of variables.

Interpretation (2) maps nicely to Jones' and Launchbury's explanation of the type of runST. The all-quantification expresses the independence of the actual state (which is fully described by the state type). The flaw in this interpretation is however the type of writeVar. As it clearly modifies the state, it should be of type ∀ s a. MutVar s a -> a -> ST t (). So this interpretation must be false.

Interpretation (1) however is not really better because it doesn't map to Jones' and Launchbury's explanation. The type ∀ s a. ST s a -> a for runST would be fine. The important thing is that there mustn't be any assumption about the concrete value of the state (of type s) which is given to the function. Hence the all-quantification shouldn't be over the state type but (instead) over the concrete value of the state. The type system must express that the result of the stateful action, which is given to runST, is independent of the state (but not independent of its type).

Hence both of my interpretations are false. I really tried to understand everything of this type construction. Is there someone who can explain that to me?

PS. I have already read the thread [How does the ST monad work? but it didn't help me. When I do the unification algorithm with my hand I see, that the mechanism works and how it works (by using the limits of scopes) but I really want to understand it – not just see that it works.

Answer 1

I would avoid interpreting s as anything concrete at all. It's basically just a “unique identifier” which ensures that the state in two different ST computations isn't mixed up. In particular, because the argument to runST is a (rank-2) polymorphic action, any state reference that you could somehow smuggle out of this monadic action would necessarily be a existential type, and there's basically nothing you can do with an unconstrained existential. So it's impossible to e.g. refer to a value in the state monad that doesn't actually exist anymore.

If you want to see s as something concrete, consider it as the type of a world in which stateful values can be allocated, modified and deleted.

Explanation of the types in that setting:

• newVar :: ∀ s a. a -> ST s (MutVar s a): on any world s, I'm able to toss a value of type a to the ground, so it can then be mangled via the MutVar reference (of course, only within the same world – though the state of this world thereby changes, but it's type / identity doesn't).
• readVar :: ∀ s a. MutVar s a -> ST s a: if the mutable reference lives in the same world as I do, I'm able to look at the object and give you a copy as the monadic result.
• writeVar :: ∀ s a. MutVar s a -> a -> ST s (): if the mutable reference lives in the same world as I do, I'm able to destroy the object sitting there and replace it with something else.
• runST :: ∀ a. (∀ s. ST s a) -> a: given an action that works on any world, I'm able to select some hidden planet nobody knows about. The action may then apply all kinds of mutating atrocities to the landscape and bring back only the result. Because nobody knew the planet, we still have a universe that, for all everybody can see, is unscathed and purely functional, but you do get the result of the destructive computation.

Answer 2

The explanation is fine, but I wonder how it maps to the final definition of the required type.

Okay, so let's back way up to what we're trying to do, and how it differs from what we can already do.

Functional state threading

We can already do functional state. This is done with the State s monad, where State s x :: * is isomorphic to the function type s -> (x, s): functions which take s as an input and return a pair containing both some value of type x for the monad and also a new state of type s. With some weak typing we could even just use a Data.Map.Strict(Map) to handle these values. For example the basic JavaScript weakly typed system has historically been enough to enable most general computation and it looks something like (omitting functions, which turn out to also be objects and have things like lexical closures to model):

data JSVariable = Undefined | Number Double | Str String | Boolean Bool | Null | 
    Object (Map String JSVariable)

With these we might use the State (Map String JSVariable) monad to store a functional namespace by which we can refer to variables, initialize them to values, and manipulate them in a state thread. And then we have a function of type

runState :: State s x -> s -> (x, s)

which we can fill in and also truncate to get:

fst . flip runState Map.empty :: State (Map a b) x -> x

More generally we might immediately be able to generalize this to make the Map be a Monoid or something.

How is ST different?

First off, ST wants to mutate an underlying data structure -- the above did not mutate the Map, but created a new Map which got passed on to the next thread. So for example if we write the equivalent of the paper's let v = runST (newVar True) in runST (readVar v) we have no ambiguity above because no matter how you slice it, the data structure that you get from the equivalent of newVar True is only a frozen-in-time snapshot of the state, not the full mutable state itself! There is no mutable state in the State s monad.

In order to maintain the facade of a distinct namespaced state (rather than some sort of global state) we keep the notion of an ST s monad, but now we do not give you direct access to that s. This means that s is something called a phantom type: it does not represent anything concrete that you can hold onto, the only value you will ever get of type s is undefined :: s, and even then, only if you consciously choose to make it.

Since we never will give you a value of type s there is no point to you ever having functions which do anything with it; for you, it will always be a type variable to be filled in by the underlying plumbing. (Let's not get into what exactly the plumbing does.)

Second, ST therefore allows a much greater range of type safety than the above weakly-typed system! We can now have each newVar :: x -> ST s (MutVar s x) return an encapsulated reference of this type MutVar s x. This reference contains a pointer to the state that it lives in, so it will never make sense in any other context -- and it also has its own distinct type x, so it can already hold any type, and it can be rigorously type-checked.

Now there be dragons

So we've started with the general idea of what we want to achieve: we want to be able to define threads of type ST s x, where s is in general left as a type variable but x is a value that we are interested in computing, and then eventually we should be able to plug them into a function which looks like:

runST' ::  ∀ s a. (ST s a) -> a

This idea "smells right" because it (a) is analogous to something similar in the State s monad, and (b) you should be able to take an ST s a, cook up a blank state for it, and then run the computation to return a purely functional a.

But... there is a problem. The problem is that at this point in the paper we have several functions like newVar :: x -> ST s (MutVar s x) which copy the internal threaded state type s into the "output" space of this monad. Even though we do not get a value of type s we still get the type variable s, which as you'll recall is some sort of general namespace for some chunk of mutable state. Other functions like readVar :: MutVar s x -> ST s x will then let you create other state threads which depend on this specific mutable state.

So that's the key word: specific. The type of newVar :: x -> ST s (MutVar s x) contains a nonspecific or general s, it will work for any s. But if you runST (newVar True) you get a MutVar s Bool for some specific s, the one that was used in the computation. We want to make sure that runST only takes general s's and not specific ones.

Put another way, newVar has type x -> forall s. ST s (MutVar s x) (see the forall that forces the variable to still be free?) while readVar has type MutVar s x -> ST s x (no forall -- by itself, or with a specific MutVar from another computation, this has a specific s to it). The s only transitions from being specific to general if for every readVar we also include the newVar that generated the object passed to readVar, to get that forall s that keeps the term general!

So the paper's essential problem is: how do we redefine ST to make sure that the state is not specific? It has to be the case that what comes out of readVar cannot be fed to runST but what comes out of newVar True and even what comes out of newVar True >>= readVar can both typecheck when fed to runST.

And their answer is, we add to the syntax of Haskell, saying "this type variable must still be a free type variable!" This is done by writing runST :: forall x. (forall s. ST s x) -> x. Notice that the forall s. is now contained within the function argument to say "hey, this parameter has to be a general, free type parameter in this expression."

This blocks the parallel-thread crap from type-checking and therefore makes the whole system correct.