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


i have came across many explanations of runst's rank 2 type , how prevents reference escaping runst. couldn't find out why prevents following code type checking (which correct still want understand how doing that):

test = v ← newstref true           let = runst $ readstref v           return true 

compared to:

test = v ← newstref true           let = runst $ newstref true >>= λv → readstref v           return true 

it seems me type of newstref same both cases: Λs. bool → st s (stref s bool). , type of v ∃s. stref s bool in both cases if understand right. puzzled @ next show why first example doesn't type check, don't see differences between both examples except in first example v bound outside runst , inside in second, suspect key here. please me show and/or correct me if wrong somewhere along reasoning.

the function runst :: (forall s . st s a) -> a magic occurs. right question ask takes produce computation has type forall s . st s a.

reading english, computation valid choices of s, phantom variable indicates particular "thread" of st computation.

when use newstref :: -> st s (stref s a) you're producing stref shares thread variable st thread generates it. means s type value v fixed identical s type larger thread. fixedness means operations involving v no longer valid "for all" choices of thread s. thus, runst reject operations involving v.

conversely, computation newstref true >>= \v -> readstref v makes sense in st thread. whole computation has type valid "for all" st threads s. means can run using runst.

in general, runst must wrap around creation of st threads. means of choices of s inside argument runst arbitrary. if context surrounding runst interacts runst's argument fix of choices of s match surrounding context , no longer freely applicable "for all" choices of s.


Comments

Popular posts from this blog

commonjs - How to write a typescript definition file for a node module that exports a function? -

openid - Okta: Failed to get authorization code through API call -

thorough guide for profiling racket code -