[解決済み] STモナドはどのように機能するのか？

質問

STモナドはIOの弟分のようなもので、IOはステートモナドに RealWorld というマジックがあります。状態をイメージすることはできるし、RealWorldが何らかの形でIOに入れられることもイメージできるのだが、型シグネチャを書くたびに ST は s のSTモナドは私を混乱させる。

例えば ST s (STArray s a b) . はどのように s はそこでどのように働くのでしょうか？ステート・モナドのステートのように参照されることなく、計算の間に人工的なデータ依存関係を構築するために使われているだけなのでしょうか（その理由は forall )?

私はただアイデアを投げかけているだけなので、私より知識のある方に説明していただけると本当にありがたいです。

どのように解決するのですか？

この s の中にあるオブジェクトを保持します。 ST モナドの外側に漏れることを防ぎます。 ST モナドの外部に漏れることを防ぎます。

-- This is an error... but let's pretend for a moment...
let a = runST $ newSTRef (15 :: Int)
    b = runST $ writeSTRef a 20
    c = runST $ readSTRef a
in b `seq` c

さて、これは型エラーです（これは良いことです！私たちが望んでいるのは STRef が元の計算の外に漏れてしまうのは困ります！)。 型エラーなのは、余分な s . 覚えておいてください。 runST には署名があることを思い出してください。

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

これはつまり s は制約がないものでなければなりません。 ですから a :

a = runST (newSTRef (15 :: Int) :: forall s. ST s (STRef s Int))

その結果、型は STRef s Int となり、これは s の外側にあるため、間違っています。 forall で runST . 型変数は常に forall の中に記述しなければなりませんが、Haskell では暗黙のうちに forall の量詞がどこでも使えるのです。 の戻り値の型を意味を持って把握できるようなルールはないのです。 a .

別の例では forall : をエスケープすることを許さない理由を明確に示すため、この例では forall をエスケープすることができない理由を明確に示すために、より単純な例を示します。

f :: (forall a. [a] -> b) -> Bool -> b
f g flag =
  if flag
  then g "abcd"
  else g [1,2]

> :t f length
f length :: Bool -> Int

> :t f id
-- error --

もちろん f id のリストのどちらかを返すので、エラーになります。 Char のリストか Int のリストと同じように、ブール値が真か偽かに応じて変化します。 これは単純に間違っています。 ST .

その一方で がなかったら s 型パラメータがなければ、コードは明らかにかなり不正確であるにもかかわらず、すべてがうまくタイプチェックされます。

STが実際にどのように動作するか。 実装的には ST モナドは実際には IO モナドと同じですが、インターフェースが少し違います。 モナドを使用するとき ST モナドを使うと、実際には unsafePerformIO またはそれと同等のものを裏側で得ています。 これを安全に行えるのは、すべての ST -関連の関数、特に forall .