1

Haskellプログラム内では、ほとんどすべての計算で何かが返され、そのような戻り値を別の計算で取得して、さらに変換を適用できることがわかっています。したがって、通常のHaskellプログラムを「フラット化」すると、次のようになります。

-- pure `a`: comes from Hask; not from file, network or any 
-- other side-effected devices

a → a' → a'' → a''' → .... → a_fin

もちろん、この純粋な値は「コンテキスト化」されている可能性があります。しかし、私たちはまだ交互の道をたどることができます：

a → m a → m a' → a'' → n a''' → ... → z a_fin

私にとって、これは、型システムや私たちの自己の欠如によって引き起こされる可能性のある副作用やその他の「驚き」を回避するためにプログラムを制御できることを示しています。しかし、がIO ()表示されると、欠落しているように見えます。

--!! What happened between the IO () and the next computation ?

a → m a → m a' → IO () >> b → b' → m b'

何も通過/受信していないようですが、IO ()少なくとも何かを読み書きする必要があります。特に「レシーバー」プロセスを検討する場合：

Sender::   a → m a → m a' → IO () >> b → b' → m b' ... → m b_fin
Receiver:: IO a' → IO a'' → IO a''' → ... → IO a_fin

a送信者では、の後に何が起こったのかを確認できませんIO ()。しかし、2つのプロセスの両方を考慮すると、欠落している部分が戻ってきます。ですから、あなたの見方によれば、私たちは情報を見逃した、または見逃していないと言うことができます。これは情報漏えいであり、プログラムに入れるときにプログラムの制御を放棄するだけIO ()ですか？

ありがとう ！

PS。ああ、そして私はまた、Receiverが純粋な値ではなく「コンテキスト化された」値でのみ計算を開始できることを発見しました。それは私の心の中で別の質問が発生します...

4

6 に答える 6

8

あなたのコメントから、IO ()型付けされた計算は有用なものを返さないため、型システムはプログラムが正しいことを保証できないと考えているようです。

まず、単純な場合を除き、型システムはプログラムの正確性を保証しません。複雑なプログラムでは、論理的な間違いを犯す可能性が十分にあり、プログラムはコンパイルされますが、間違った結果が返されます。論理エラーを回避するのはプログラマーの義務であり、型システムは 1 つの (確かに強力な) ツールです。

2 番目のポイントは最初のポイントに続きます。IO単純なモナドです。これは (もちろん、型システムの観点からは) 他の型と同じ型です。私の知る限り、型システムから特別な扱いを受けることはありません。type の値は、IO ()「実行されたときに何らかの形で外界に影響を与える可能性があり、意味のあるものを何も生み出さない不純な計算」を意味し、それ以上の意味はありません。type の値を考えてみましょうState Int (): これは、「実行時に type の現在の状態で何かを行う可能性があり、Int有用なものを何も生成しないステートフルな計算」を意味します。ご覧のとおり、これらの値にはどちらも何らかの副作用があり、計算結果に関して同じ意味を持っています。. このように、型システムの観点からは同等です。しかし、2 つ目は完全に純粋な計算です。またはを使用して、意味のある値 (この場合はInt)に簡単に変換できます。execStaterunState

于 2012-06-29T17:53:21.887 に答える
3

いいえ、チェーン内の各アクションは直前のアクションの結果しか見ることができないと考えています。しかし実際には、各アクションは、必要に応じて、前のアクションの結果にアクセスできます。おもちゃの例を使用するだけです：

return 5 >>= (\x -> putStrLn "mwahaha!" >>= (\_ -> putStrLn "x is " ++ show x >>= (\_ -> return ())))

変数のスコープに注意してくださいx— 式全体の最後まで拡張されます。(括弧は省略可能ですが、範囲を明確にするために入れています。)

の型をもう一度考えてみましょう>>=:

(>>=) :: Monad m => m a -> (a -> m b) -> m b

m aこれは、「タイプのアクションの結果とタイプの関数を使用して、プログラムの残りの部分a -> m bを構築する」という言い換えになります(次のアクションだけではありません)。

アクションには、変更可能なメモリと、プログラムで使用可能な I/O デバイスへのコンテキストもあります。これは、アクションが別のアクションと通信できるもう 1 つのメカニズムでもあります。タイプ の 2 つのアクションはIO ()、ご存じのとおり、共有メモリを介して、またはファイルを共有することによって通信できます。

于 2012-06-29T16:02:55.880 に答える
1

はい、特定の観点から見ると、タイプの値はIO aどこからともなく情報を引き出します。それらを生成した関数への入力に由来しない情報。の全体的なポイントはIO、結果がプログラムの外の世界に依存する（そして影響を与える可能性がある）計算を書くことであるため、これは避けられません。への呼び出しから得られる情報readFileは、プログラムではなく、ディスク上のファイルに存在します。IOつまり、アクションを使用するプログラムの結果は、作成しているプログラムの制御下にないものに依存するという意味で、「制御を放棄」しています。しかし、すべてのプログラムはこのようなものです。それを回避する唯一の方法は、使用しないことですIO(または外部の世界と通信する任意のメカニズム) がまったくない場合、プログラムは、最終結果が何であれ、非常に複雑な方法で書き留めることができます。

しかし、型システムは実際の入力/出力値を気にすることIOはなく、関与していない場合でも、それらが正しいことを証明しません。型の関数の型チェックでInteger -> Stringは、実際に を受け入れてIntegerを返す操作で実装されていることを確認するだけですString。正しい文字列が生成されるかどうかという概念はありません。

型システムに「嘘をつく」ことさえできます。は、任意のundefined関数の有効な定義です。これにより、型システムに関する限り、たとえば整数を取り、文字列を返す関数が得られます。しかし、それはその機能の正しい実装であるという意味ではありません。これに関して定義された他の関数も正しくなく、型チェッカーはまったく気にしません。

同様に、タイプの関数は、関数が を受け入れてを生成するInteger -> IO ()演算を使用することをチェックします。型チェックが証明するのはそれだけであり、これはforやfor 、または他の型と同じです。IntegerIO ()IO ()IO IntegerInteger

于 2012-07-01T23:55:03.520 に答える
0

IO ()は、計算が過去のアクションの影響を受ける可能性があること、および「計算チェーン」内のIO将来のアクションに影響を与える可能性があることを意味します。IOただし、それに続く非 IO 値 (モナド スタックがある場合、スタック内のどこにも IO がないもの) は直接影響を受けることはありません()。影響を受けるものに依存している場合、間接的に影響を受ける可能性がありますIO a。これは を無視しunsafePerformIOており、上記の説明が依然として本質的に当てはまるような方法でのみ使用する必要があります。

于 2012-06-29T19:01:58.347 に答える
0

このチェーンは、プログラムの「状態」で構成されています (まあ、一種の)。簡単なプログラムを考えてみましょう:

main = do
  let a = 4  -- 1
  print a    -- 2
  print a    -- 3

ここで、ステップ 1 の後、あなたの状態は4です。しかし、ステップ 2 の後、これ4は消えません — 現在の状態は (4, ()) です。ステップ 3 の後は (4, (), ()) などです。

簡単に言えば、後で使用される情報はチェーンに残ります。の後に消えませんIO ()。

于 2012-06-29T10:46:40.873 に答える
0

質問が何であるかはよくわかりませんが、とにかく私の直感が正しい場合に答えを入れます.

実際のところ、プログラムの構成関数の型だけを見ると、次の 2 つの結論のいずれかに到達できます。

  1. プログラムは IO を使用しないため、計算は純粋であることが保証され、副作用は発生しません (もちろん、特定の制限内で)。

また

  1. あなたのプログラムは IO を使用しているため、純粋ではなく、副作用が発生しないという保証はありません。

もちろん、可能なすべての IO 計算の範囲内に、副作用を生じない計算があります。これは、タイプが純粋性を示しているが、 などの安全でない関数を使用している計算があるのと同じunsafePerformIOです。しかし、一般に、純粋関数のタイプを見て、次のように言うことができます。この関数は、ディスク IO、ネットワーク IO、またはその他の種類のものでは失敗しません。同じ保証は IO 計算には当てはまりません。

于 2012-06-29T13:57:57.403 に答える