モナド・トランスでリフティングが必要なのはいつですか？

Question

モナド・トランスを学んでいますが、リフトを使う必要があるときは混乱しています。 次のコードがあるとします（これは面白いことではありません。デモンストレーションでは最も簡単なコードです）。

foo :: Int -> State Int Int 
foo x = do 
    (`runContT` pure) $ do 
    callCC $ \exit -> do 
     when (odd x) $ do 
     -- lift unnecessary 
     a <- get 
     put $ 2*a 
     when (x >= 5) $ do 
     -- lift unnecessary, but there is exit 
     a <- get 
     exit a 
     when (x < 0) $ do 
     -- lift necessary 
     a <- lift $ foo (x + 10) 
     lift $ put a 

     lift get 

だから、メインDOブロックがContT Int (StateT Int Identity) Intを入力したモナドスタックは、そこにあります。

ここで、第3のwhenは再帰でブロックします。プログラムをコンパイルするにはリフトが必要です。 2番目のブロックでは、揚力は必要ありませんが、どういうわけか、線の上にある線をContTにするように、exitの存在が原因であると思います。しかし、最初のブロックでは、持ち上げる必要はありません。 （ただし明示的に追加しても問題ありません）これは本当に私にとって混乱しています。私はすべてのwhenブロックが同等であると感じて、リフトはどこにでもどこにも必要であるはずです。しかし、それは明らかに真実ではありません。エレベーターの必要/不要の主な違いはどこですか？

Answer 1

使用しているモナドトランスライブラリが少し巧妙であるため、ここで混乱が生じています。具体的には、getおよびputのタイプは、StateまたはStateTと明示的には言及していません。むしろ、彼らはそのため限り、我々はMonadState実装するモナドに関連してこれを使用すると、明示的なliftのための必要はありませんライン

get :: MonadState s m => m s 
put :: MonadState s m => s -> m() 

に沿っています。これは、あなたがget/put

instance MonadState s (StateT s m) 
instance MonadState s m => ContT k m 

以来、両方のホールドを使用するすべてのインスタンスの場合です。言い換えれば、型クラスの解決は自動的に適切なリフティングを行うことを処理します。これは、プログラム終了時に get/ putの liftを削除できることを意味します。

型が明示的にState Int Intであるため、これは再帰呼び出しでは発生しません。もしあなたがMonadState Int m => m Intに一般化すれば、あなたはこの最終的な持ち上げをなくすことさえできます。

Answer 2

私は、表面的であると同時に重要なすべての代替的な答えを提供したいと思います。

liftは、そうでない場合はチェックしないと、liftを使用する必要があります。

はい、それは表面的に聞こえ、深い意味がないようです。しかしそれは事実ではありません。 MonadTransは、モナドのアクションをより大きなコンテキストに中立的に持ち上げることができるクラスです。クラスの法則は、技術的な記述が必要な場合には、「中立」の意味をより明確に規定しています。しかし、結局のところ、liftは、提供されたアクションを別のタイプと互換性を持たせるために必要なものを超えて何もしません。

だから - liftは何をしますか？モナドアクションをより大きなタイプに持ち上げるために必要なロジックを提供します。あなたはそれをいつ使う必要がありますか？より大きなタイプに持ち上げる必要があるモナドのアクションがあるとき。あなたはより大きなタイプに持ち上げる必要があるモナドの行動はいつ持っていますか？それはタイプがあなたに伝えるものです。

これはHaskellを使用するための重要な部分です。コードの理解をモジュール化することができます。タイプシステムはあなたのために巨額の簿記を追跡します。簿記権を得るためにそれに頼ってください、あなたはあなたの頭の中に論理を保つ必要があります。コンパイラとタイプシステムは、精神的なアンプとして動作するようになっています。彼らが世話をするほど、ソフトウェアを書く際に頭を悩ます必要が少なくなります。