トランススタックでSTTモナドをアンラッピングしますか？

Question

この質問は明らかに、hereとhereで説明されている問題に関連しています。残念ながら、私の要求はそれらの質問とは少し異なり、与えられた答えは私には当てはまりません。私も実際に理解していませんなぜrunSTはこれらのケースではタイプチェックに失敗しますが、これは役に立たない。

私の問題はこれです、私は1つのモナドスタック、またはむしろ単一モナドを使用するコードのいずれかのセクションがあります。

import Control.Monad.Except 
type KErr a = Except KindError a 

をコードする別のセクションには、STT monad以内にこれをラップし、このと統合する必要があります。

type RunM s a = STT s (Except KindError) a 

これらのセクションの間のインターフェイスでは、明らかに外側レイヤーをラップして展開する必要があります。私はKErrで動作するように、以下の機能を持っている - >RunM方向：

kerrToRun :: KErr a -> RunM s a 
kerrToRun e = either throwError return $ runExcept e 

が、私はちょうど逆はチェックを入力することができません何らかの理由：

runToKErr :: RunM s a -> KErr a 
runToKErr r = runST r 

アイムRunMの内部モナドがKErrと同じ構造をしていると仮定すると、STT層のラップを解除した後に戻すことはできますが、これまでのところは得られないと思われます。runSTは文句を言っています型引数について：

src/KindLang/Runtime/Eval.hs:18:21: 
    Couldn't match type ‘s’ with ‘s1’ 
     ‘s’ is a rigid type variable bound by 
      the type signature for runToKErr :: RunM s a -> KErr a 
      at src/KindLang/Runtime/Eval.hs:17:14 
     ‘s1’ is a rigid type variable bound by 
      a type expected by the context: 
      STT s1 (ExceptT KindError Data.Functor.Identity.Identity) a 
      at src/KindLang/Runtime/Eval.hs:18:15 
    Expected type: STT 
        s1 (ExceptT KindError Data.Functor.Identity.Identity) a 
     Actual type: RunM s a 

私も試してみた：より強く、問題の原因だった場合には、その期待される戻り値の型からrunSTを分離するために

runToKErr r = either throwError return $ runExcept $ runST r 

を、が、結果は同じです。

s1のタイプはどこから来ていますか.GHCにはsと同じタイプがあると説得するにはどうすればよいですか？

Answer 1

（以下ST s aに関する交渉が、ちょうど同じSTT s m aとして適用され、私は以下のトランスバージョンの話の不必要な複雑化を回避しました）

あなたが見ている問題はrunSTがに(forall s. ST s a) -> aを入力していることです外部の純粋な世界からの計算の潜在的な影響（STRef変更）を分離してください。 ST計算、STRefsなどにタグが付けられているsファントムタイプの全体のポイントは、それらが属する「ST -domain」を追跡することです。 runSTのタイプは、ドメイン間で何も通過できないことを保証します。

あなたが同じ不変を強制することにより、runToKErrを書き込むことができます。

{-# language Rank2Types #-} 

runToKErr :: (forall s. RunM s a) -> KErr a 
runToKErr = runST 

（もちろん、あなたはこの制限は、あなたが書くことを望むプログラムのために強すぎること、さらに道を実現するかもしれません。その時点であなたは申し訳ありませんが、私はあなたのプログラムを再設計する必要があることを意味する希望を失う必要があります。私はsとaの与えられた選択肢のためにあなたST s aを渡すと、それがあるため、エラーメッセージについては、あなたは「s1とsが同じ型であることを型チェッカーを納得させる」ことができない理由がある）

あなた自身にsを選択させるようなものを与えるのと同じではありません。 GHCはs1（Skolemized変数）をsと選択し、とST s1 a