STモナドはどのように機能しますか？

Question

私は、STモナドはIOの弟のようなものであることを理解しています。これはRealWorldの魔法を追加した状態のモナドです。私は状態を描くことができ、RealWorldは何とかIOに入れられると想像することができますが、STのタイプシグネチャを書き込むたびに、STモナドのsが私を混乱させます。

例えば、ST s (STArray s a b)とする。 sはどのように機能しますか？これは、状態モナドの状態のように（forallのために）参照することができなくても、計算間の人為的なデータ依存関係を構築するために使用されていますか？

私はちょうどアイデアを捨てて、私はそれを私に説明するよりも知識のある人に本当に感謝しています。

Answer 1

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 :: (forall s . ST s a) -> a 

これは、あなたが実行している計算上のsが、それには何の制約を持たないために持っていることを意味しますrunSTが署名を持っていることを覚えておいてください。ですから、aを評価しようとすると：sはrunSTにforallの外側を「エスケープ」しているので

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

結果が間違っているタイプSTRef s Intを、持っているでしょう。型変数は常にforallの内部に現れなければならず、Haskellは暗黙的にforall個の量子を許しています。意味のある返り値の型をaから把握できるようにするルールはありません。

別の例forallで：あなたは物事がforallを逃がすことができない理由を明確に示すために、ここでは単純な例である：それは戻ってくるので、

もちろん f idの

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 -- 

は、エラーになりますブール値が真であるか偽であるかに応じて、CharのリストまたはIntのリストのいずれかです。 STの例のように、間違っているだけです。

一方、sタイプのパラメータがない場合は、コードが明らかにかなり偽であるにもかかわらず、すべてがタイプチェックされます。 STは、実際にどのように動作する

：実装面を、STモナドは実際にIOモナドとしてではなく、わずかに異なるインターフェイスと同じです。 STモナドを使用すると実際にunsafePerformIOまたはそれと同等のものが得られます。これを安全に実行できる理由は、すべてのST関連の関数、特にforallの部分の型シグネチャが原因です。

Answer 2

sは、タイプシステムが安全ではないことをやめさせるハックです。実行時には何もしません。型チェッカーは、疑わしいことをするプログラムを拒否させるだけです。 （これはいわゆるファントムタイプであり、タイプチェッカーの頭にのみ存在し、実行時には何も影響しません）