ST参照は透過的ですか？

Question

なぜSTは次のコードを許可しないように設計されていますas shown in the wikibook？この記事では、STのエフェクトが別のSTに漏れることが示唆されていますが、なぜそれは本当に理解できません。

私は特定のST s (STRef s a)を実行できないようです。 STエフェクトは含まれていますが、参照は透過的ですが、そのような使用は無効と見なされますか？

直観は1 IO、多くの独立したSTがあることに関連IOとSTの意味の違いがあることを私に語ったが、私はよく分かりません。

> runST (newSTRef True) 

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

> :t newSTRef 
newSTRef :: a -> ST s (STRef s a) 

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

Answer 1

もっと質問自体よりも、質問のタイトルへの答えが、それでも：

はい、STは参照透明です。これは単なる推測と信じられていた長い間

、そして唯一の今年、私たちはそのための適切な証拠を持っている：

州の単項カプセル化のための論理的関係：runSTの存在下で、文脈等価性を証明
アミンTimany、レオStefanesco、モーテン・クロ-Jespersen、ラースBirkedal
条件付きで、私は本当にunderstaない2018
http://iris-project.org/Preprint PDF

Answer 2

をPOPLする受け入れあなたが求めているものは何ですか、私はあなたの質問ふりをするつもりです：

なぜrunST (newSTRef True)を禁止するように設計されているのですか？

ことが許可された場合、それはもはや参照透明ないだろう：

main = do 
    let r = runST (newSTRef True) 
    evaluate (runST (writeSTRef r False)) 
    print (runST (readSTRef r)) 

このコードは考え出力False。

main = do 
    evaluate (runST (writeSTRef (runST (newSTRef True)) False)) 
    print (runST (readSTRef (runST (newSTRef True)))) 

このコード（ユーザ毎にrをインライン化した結果）が出力True、希望runST (newSTRef True)の各インスタンスは、新規STRef変数を割り当てるからです。

実際にrunSTの方法が実装されているため、ST sアクション内に割り当てられたすべてのリソースがそのアクションをエスケープできません。

IOとの違いは、runIOの機能がないということです。複数の独立したIOアクションを作成することはできますが、runIO（それらは単なる値）なしでは関係ありません。実際にIOアクションを実行する唯一の方法は、mainにバインドし、ランタイムシステムにそれを拾い上げさせることです（暗黙的なrunIOがmainにラップされているようなものです）。IOというアクションが1つしかありません。プログラム。

もちろん、この単一のアクションは複数の小さなアクションを組み合わせることで構成できますが、最終的にはまだモノリスです。一方、runSTは、複数のアクションを独立して実行できるようにします。