RunST prevents accessing the reference of another stateful thread in a closure

I have came across many explanations of RunST's Rank 2 type and how it prevents the reference from escaping RunST. But I couldn't find out why this also prevents the following code from type checking (which is correct but I still want to understand how it is doing that):

test = do v ← newSTRef True
          let a = runST $ readSTRef v
          return True

Compared to:

test = do v ← newSTRef True
          let a = runST $ newSTRef True >>= λv → readSTRef v
          return True

It seems to me that the type of newSTRef is same for both cases: Λs. Bool → ST s (STRef s Bool). And the type of v is ∃s. STRef s Bool in both cases as well if I understand it right. But then I am puzzled at what to do next to show why the first example doesn't type check, I don't see differences between both examples except that in the first example v is bound outside runST and inside in the second, which I suspect is the key here. Please help me show this and/or correct me if I am wrong somewhere along my reasoning.

Answers


The function runST :: (forall s . ST s a) -> a is where the magic occurs. The right question to ask is what it takes to produce a computation which has type forall s . ST s a.

Reading it as English, this is a computation which is valid for all choices of s, the phantom variable which indicates a particular "thread" of ST computation.

When you use newSTRef :: a -> ST s (STRef s a) you're producing an STRef which shares its thread variable with the ST thread which generates it. This means that the s type for the value v is fixed to be identical to the s type for the larger thread. This fixedness means that operations involving v no longer are valid "for all" choices of thread s. Thus, runST will reject operations involving v.

Conversely, a computation like newSTRef True >>= \v -> readSTRef v makes sense in any ST thread. The whole computation has a type which is valid "for all" ST threads s. This means it can be run using runST.

In general, runST must wrap around the creation of all ST threads. This means that all of the choices of s inside the argument to runST are arbitrary. If something from the context surrounding runST interacts with runST's argument then that will likely fix some of those choices of s to match the surrounding context and thus no longer be freely applicable "for all" choices of s.


Need Your Help

Programatically show hide button in drupal

php drupal drupal-7

I've got a sign up page with an anchor button for signing up, but when a user is logged in the form is hidden but the content should still be visable just hiding the join now button, im trying to d...

latest 50 documents from mongodb

performance mongodb

In order to show latest 10 news to user My application is fetching all news from collection news and then I am sorting them on date field of document and displaying them top 10.

About UNIX Resources Network

Original, collect and organize Developers related documents, information and materials, contains jQuery, Html, CSS, MySQL, .NET, ASP.NET, SQL, objective-c, iPhone, Ruby on Rails, C, SQL Server, Ruby, Arrays, Regex, ASP.NET MVC, WPF, XML, Ajax, DataBase, and so on.