25

証明

このブログ投稿では、Tekmoは、それがそのコンストラクターのファンクターのようなものであるため（私は推測します）、それが終了することを証明できることを指摘していますExitSuccess（それはそのように動作Constしません）。xfmapconst

オペレーショナルパッケージを使用すると、Tekmoは次のTeletypeFように翻訳される可能性があります。

data TeletypeI a where
    PutStrLn :: String -> TeletypeI ()
    GetLine :: TeletypeI String
    ExitSuccess :: TeletypeI ()

運用は無料のモナドと同型であることを読みましたが、ここでそれが存在することを証明できExitSuccessますか？それはまったく同じ問題を抱えているように私には思えますexitSuccess :: IO ()、そして特に私たちがそれのためにインタプリタを書くなら、それが終了しなかったかのようにそれを書く必要があるでしょう：

eval (ExitSuccess :>>= _) = exitSuccess

パターンワイルドカードを含まない無料のモナドバージョンと比較してください。

run (Free ExitSuccess) = exitSuccess

怠惰

オペレーショナルモナドチュートリアルで、apfelmusは欠点について言及しています。

s->（a、s）として表される状態モナドは、次のようないくつかの無限のプログラムに対処できます。

evalState (sequence . repeat . state $ \s -> (s,s+1)) 0

一方、命令リストアプローチでは、最後のReturn命令のみが値を返すことができるため、これを処理する見込みはありません。

これは無料のモナドにも当てはまりますか？

4

3 に答える 3

16

（前の答えを大胆に組み合わせて大賞をすくうことができます。;-)）

重要な観察はこれです：正確に何を証明しますか？に関する定式化Free TeletypeFにより、次のことを証明できます。

タイプのプログラムのすべてのインタプリタは、命令Free TeletypeF aに遭遇したときに終了する必要があります。ExitSuccess言い換えれば、私たちは自動的に代数の法則を取得します

 interpret (exitSuccess >>= k) = interpret exitSuccess

したがって、Freeモナドを使用すると、特定の代数法則をタイプに組み込むことができます。

対照的に、運用アプローチはのセマンティクスを制約せず、ExitSuccessすべてのインタプリタに関係する関連する代数法則はありません。この命令に遭遇したときに終了するインタープリターを作成することは可能ですが、そうでないインタープリターを作成することもできます。

もちろん、ワイルドカードパターンマッチを使用しているなどの理由で、特定のインタプリタが検査によって法律を満たしていることを証明できます。Sjoerd Visscherは、の戻り型をに変更することで、型システムでこれを強制できることを確認していExitSuccessますVoid。ただし、これは、無料のモナドに焼き付けることができる他の法則、たとえば、mplus命令の分配法則では機能しません。

したがって、混乱を招くような出来事の中で、「無料」を「代数法の最小量」と解釈すると、運用アプローチは無料のモナドよりも無料になります。

また、これらのデータ型が同型ではないことも意味します。ただし、これらは同等です。で記述されたすべてのインタプリタは、で記述Freeされたインタプリタに変換できProgram、その逆も可能です。

個人的には、すべての法律を通訳に入れるのが好きです。なぜなら、無料のモナドに焼き付けることができない法律がたくさんあり、それらすべてを1か所にまとめるのが好きだからです。

于 2013-01-12T16:45:25.280 に答える
11

答えは「はい」ですが、次の別の翻訳を使用する場合に限りますTeletypeF。

data TeletypeI a where
    PutStrLn :: String -> TeletypeI ()
    GetLine :: TeletypeI String
    ExitSuccess :: TeletypeI Void

の引数はTeletypeI、操作がプログラムの残りの部分に提供する/提供する必要があるものです。の継続の議論のタイプkです

eval (ExitSuccess :>>= k) = ...

タイプの値がないため、それが呼び出されるVoidことkはありません。（いつものように、undefinedここでは無視する必要があります。）

同等のタイプは次のとおりです。

data TeletypeI a where
    PutStrLn :: String -> TeletypeI ()
    GetLine :: TeletypeI String
    ExitSuccess :: TeletypeI a

ここでk、任意のタイプに一致する値を提供する必要がありますが、それもできません。singleton ExitSuccessフレキシブルタイプになっているので、これはより実用的Program TeletypeI aです。

同様に、タイプ、またはexitSuccessを指定することで修正できます。IO VoidIO a

于 2013-01-10T19:54:02.387 に答える
5

答えはノーです。操作上のプログラムが上のプログラムの残りの部分を無視していることを証明することはできませんexitSuccess。と比較TeletypeIしTeletypeFて、理由を確認してください。TeletypeF比較しやすいようにGADT表記で書き直します

data TeletypeF x where                     | data TeletypeI x where
  PutStrLn :: String -> x  -> TeletypeF x  |   PutStrLn :: String -> TeletypeI ()
  GetLine :: (String -> x) -> TeletypeF x  |   GetLine :: TeletypeI String
  ExitSuccess ::              TeletypeF x  |   ExitSuccess :: TeletypeI ()

を使用してTeletypeF、実際のプログラムをすぐに作成できます。

GetLine (\str -> PutStrLn (map toUpper str) ExitSuccess)

TeletypeI同じように「プログラムの残りの部分」を参照する方法はありTeletypeFません。

-- TeletypeF:
GetLine (\str -> "rest of program" goes here)
-- or
PutStrLn someString ("rest of program" goes here)
-- or
ExitSuccess -- there is no "rest of program" slot provided

このTeletypeI「プログラムの残りの部分」の情報が不足しているため、に遭遇したときに知識を得ることができなくなりますExitSuccess。

-- TeletypeI
PutStrLn someString -- no information about "rest of program"
-- or
GetLine -- no information about "rest of program"
-- or
ExitSuccess -- no information about "rest of program"

「プログラムの残りの部分」として来ることが許されるのは、Programそれが適用されている命令セットについて何も知らないタイプ次第です。単に命令をバインドし、を介して終了することができますReturn。

于 2013-01-10T18:48:40.793 に答える