runSTの型

Lazy Functional State Threads（http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.144.2237&rep=rep1&type=pdf）を読んだので、メモしておく。 runSTは特徴的な型を持っているけれど、それはどうやらスレッド的な安全性のためらしい。文章で色々書いても分かりにくいから、実際にコードを書いて確認。引用部は『Lazy Functional State Threads』から引っ張って来た。訳は少し意訳気味（正しいとは言ってない）。また、型を示す時に、説明のために少しおかしなことになっているが、何を意図しているか察してほしい。

runSTは、

runST :: forall a. (forall s. ST s a) -> a

という型を持つ。

runST :: forall s a. ST s a -> a

でなくそのような型定義にしなければならないのは、次のような問題があるかららしい。

What is to prevent a reference from one thread being used in another?

訳：あるスレッドからの参照が他のスレッドで使われるのを防ぐにはどうすればよいか。

というのも、

Doing so would be a great mistake, because reads in one thread are not sequenced with respect to writes in the other, and hence the result of the program would depend on the evaluation order used to execute it.

訳：それができてしまったなら、それは大きな欠陥だ。なぜなら、あるスレッドでの読み込みと、他のスレッドでの書き込みの順序が決まらないために、プログラムの実行結果が実行時の評価順序によって変わってしまうからだ。

そこで、そのような操作が行われていないか確認する必要がある。runSTの型定義により、上記のような操作が行われていないことを、実装が難しい実行時チェックでなく、単なる型チェックで確認することができるらしい。

例えば、

let
    v = runST (newVar True)
in
    runST (readVar v)

のようなコードは、一行目のスレッドから参照を取り出し、三行目のスレッドで使っているので、欠陥がある。このコードの型チェックを考えてみると、三行目のreadVar vの型は、v :: MutVar s Bool |- readVar v :: ST s Boolとなる。ここで、sは自由変数（一行目に依存している）なので、runST :: forall a. (forall s. ST s a) -> aのforall s.で束縛できない。

次にそもそも、

let v = runST (newVar True)

によって、参照が外部に漏れ出していることが諸悪の根源であるので、これも型チェックで弾ければ良い。実際に確かめてみる。 newVar Trueの型はnewVar True :: forall s. ST s (MutVar s Bool)であるので、runST (newVar True) :: (forall s. ST s (MutVar s Bool)) -> (MutVar s Bool)となる。しかし、一番右のsが、sのスコープ(forall s. ST s (MutVar s Bool))から出てしまっているので、エラーとなる。ghciで実行してみると、

*Main Data.STRef Control.Monad.ST> runST $ newSTRef 1

<interactive>:210:9: error:
    • Couldn't match type ‘a’ with ‘STRef s a0’
        because type variable ‘s’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          ST s a
        at <interactive>:210:1-18
      Expected type: ST s a
        Actual type: ST s (STRef s a0)
    • In the second argument of ‘($)’, namely ‘newSTRef 1’
      In the expression: runST $ newSTRef 1
      In an equation for ‘it’: it = runST $ newSTRef 1
    • Relevant bindings include it :: a (bound at <interactive>:210:1)

というエラーが出る。

このようにして、型チェックの段階で欠陥となりうる操作を弾くことができている。

参考までに、runST :: forall a s. (ST s a) -> aという型定義ではどのような振る舞いをするのか考察しておく。 上と同じ順番で見ていくと、

let
    v = runST (newVar True)
in
    runST (readVar v)

ここで、readVar vの型はv :: MutVar s Bool |- readVar v :: ST s Boolとなる。ここで、sは自由変数（一行目に依存している）であるが、runST :: forall a s. ST s a -> aに適用でき、その型はrunST (readVar v) :: ST s Bool -> Boolとなる。

また、

let v = runST (newVar True)

も、newVar True :: forall s. ST s (MutVar s Bool)であるので、runST (newVar True) :: ST s (MutVar s Bool) -> (MutVar s Bool)となって、エラーにならない。

さて、では実際にrunSTを使ってみる。

hoge x = runST (do w <- newSTRef x; readSTRef w)

:t \x -> do w <- newSTRef x; readSTRef w --> b -> ST s b

hoge 1 --> 1
hoge () --> ()

ここで定義したhogeは恒等関数idと同じ意味を持つ。一方でreturnを使うと、

fuga x = runST (do w <- newSTRef x; return w)

:t \x -> do w <- newSTRef x; return w --> a -> ST s (STRef s a)

<interactive>:271:37: error:
    • Couldn't match type ‘a’ with ‘STRef s t’
        because type variable ‘s’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          ST s a
        at <interactive>:271:10-45
      Expected type: ST s a
        Actual type: ST s (STRef s t)
    • In a stmt of a 'do' block: return w
      In the first argument of ‘runST’, namely
        ‘(do { w <- newSTRef x;
               return w })’
      In the expression:
        runST
          (do { w <- newSTRef x;
                return w })
    • Relevant bindings include
        w :: STRef s t (bound at <interactive>:271:20)
        x :: t (bound at <interactive>:271:6)
        fuga :: t -> a (bound at <interactive>:271:1)

とエラーになる。このように、参照を外部に出すことはできないし、stateも外部に出すこともできない。まあ、stateを外部に出すことができないから、参照を外部に出すことができないのだが。スレッド内部で状態を持つことはできても、そのことによる副作用はスレッド内部に閉じ込められる（encapsulation？）から、参照透明性を維持できるのだろう。実際、hogeは「どのような順番」で「何回呼ばれても」与えられた値に対して同じ操作を行う。

追記

let v = runST (newVar True)

の部分がエラーになることの説明が、原典と違うと思います。これは、僕なりの解釈なので間違っていたら教えてください。