別のモナドガイド（パート3：モナドの法則）

マイク・ヴァニエ

前の記事で、 モナド型クラスの2つの基本的な単項演算について説明しました。バインド演算子（バインド、 >> = ）と戻り関数です。 この記事では、 モナド型クラスの定義に至り 、モナドの法則について説明します。

完全なモナド型クラス

Monad型クラスの定義全体を見てみましょう。

クラス Monad m ここで
（ >> = ） :: m a -> （ a- > m b ） -> m b
return :: a- > m a
（ >> ） :: m a- > m b- > m b
fail :: 文字列 -> m a

よく知られているのは、同じタイプの>> =演算子とreturn関数ですが、それらに加えて>>演算子とfail関数もあります。 彼らはどういう意味ですか？

失敗関数は、最初はエラーを報告する非常に原始的な方法です。 >> =演算子が一致エラーのためにタイプaの値をタイプa-> mbの関数にバインドできない場合に呼び出されます。 退屈なため、このメカニズムの詳細には触れません。 必要に応じて、 Haskell Webサイトのドキュメントを参照してください。 ほとんどの場合、 失敗の心配は必要ありません。

>>演算子はもう少し興味深いものです。 彼はこのタイプを持っています：

（ >> ） :: m a- > m b- > m b

この演算子は、単項シーケンス演算子です。 特に、モナドアプリケーションの変形（ >> =または「バインド」）で、タイプmbの 「アクション」を実行する前に、タイプaのアンパックされた値を破棄します。 次のように定義されます。

mv1 >> mv2 = mv1 >> = （ \ _- > mv2 ）

ここで、モナド値mv1からアンパックされた値はすべて拒否され、最終的なモナド値mv2が返されることがわかります。 演算子は、展開された値の型が（）の場合、つまり空の型である場合に役立ちます。 putStrLn関数は良い例と考えることができます。

putStrLn :: 文字列 -> IO （ ）

2行を次々に印刷し、各行の後に改行を入れたいとします。 これを行うことができます：

putStrLn 「これはストリング1です。」 >> putStrLn "これは文字列2です。"

そして、なぜこれが機能するのですか？ タイプを見てみましょう。

（ putStrLn "これは文字列1です。" ） :: IO （ ）
（ putStrLn "これは文字列2です。" ） :: IO （ ）

つまり、 >>演算子は、タイプIO（）の 2つのモナド値を、タイプIO（）の 1つの結果のモナド値に結合します。 >>演算子を使用して、このケースに特化してみましょう。

（ >> ） :: m a- > m b- > m b

mがIOで、 aとbが（）の場合、次のようになります。

（ >> ） :: IO （ ） -> IO （ ） -> IO （ ）

書くことで、おそらく、 >>演算子が2つの「アクション」を連続して実行する、つまり行を出力すると言うことができます。

より複雑な例です。 端末からテキスト行を読み取り、2回印刷する必要があります。 次のようにできます。

readAndPrintLineTwice :: IO （ ）
readAndPrintLineTwice = getLine >> = （ \ s -> （ putStrLn s >> putStrLn s ） ））

演算子の優先順位のため、レコードは角括弧なしで残すことができます。

readAndPrintLineTwice :: IO （ ）
readAndPrintLineTwice = getLine >> = \ s- > putStrLn s >> putStrLn s

これはどういう意味ですか？ getLine-モナド値（「アクション」）。端末からテキスト行を読み取ります。 >> =演算子は、この文字列をモナド値から「アンパック」し、名前sに関連付けます（ \ s-> putStrLn s >> putStrLn sは、モナド関数、 >> =演算子の2番目の引数であるため）。 次に、 sという行が、モナドの値putStrLn s >> putStrLn sによって使用され、連続して2回出力されます。

あなたが言うことが神秘的に思えるなら、それはあなたのせいではありません。 ここで奇妙なことが起こっていますが、ステートモナドについて話をするまでは説明できません。 しかし、今では 、まだどのように起こっているのかを完全に理解していない場合でも、 何が起こっているのかを追跡できなければなりません。

今、少し戻ってモナドの法則を見ていきます。 これらは、特定のモナドごとに>> =演算子と戻り関数を使用する際に大きな役割を果たします。 その後、より実用的な資料に移ります。

モナディズムの三法則

多くの重要な法則は3つのグループに分類されます。ニュートンの3つの機械法則、熱力学の3つの法則、Azimov Roboticsの3つの法則、惑星運動の3つのケプラー法則などです。 もちろん、「3つのモナドの法則」が何よりも重要であることを除いて、このモナドは違いません。 ;-)

>> =演算子と戻り関数が特定のモナドに対して有効であるためには、それらはそのモナドに対して正しい型を持たなければなりません。 したがって、たとえば、定義>> =およびMaybeモナドの戻り値には、そのタイプが含まれます。

（ >> = ） :: たぶん a -> （ a- > たぶん b ） -> たぶん b
return :: a- > たぶん a

そして、モナドの場合、 IOにはIOタイプが含まれます

（ >> = ） :: IO a -> （ a- > IO b ） -> IO b
return :: a- > IO b

ただし、これでは十分ではありません。 これらの関数/演算子は、3つの「モナドの法則」を満たすためにも必要です。 モナドの法則は実際には非常に単純です。 これらは、モナド構成が予測可能な方法で機能するように設計されています。 最初にモナドの法則の「素敵な」バージョンを提供し、次に通常説明されているように（ugい）方法を示します。 （ありがとうございます。「素敵な」オプションの方がずっと理解しやすいです。）

素敵なバージョン

以下は、モナド合成の観点から表現された3つのモナド則の素晴らしい定義です（演算子（> =>）は関数合成のモナド演算子であることを思い出してください）：

1 return > => f == f
2 。 f > => return == f
３ 。 （ f > => g ） > => h == f > => （ g > => h ）

これらの法律は私たちに何を伝えていますか？

規則1と2は、 戻り値を指定します。これは、関数の単項合成の単位（中立要素）です（最初の規則は、戻り値が左側の単位で、2番目の規則が右側の単位であることを示します）。 つまり、単項関数fを作成して （任意の順序で）返すと、単に関数fが返されます。 アナログは、0-整数を加算する機能の中立要素、1-整数乗算機能の中立要素と見なすことができます。 いずれの場合も、対応する関数を使用して通常の値に接続されたニュートラル要素は、この値を単純に返します。

法則3は、合成の単項関数は結合的であると述べています。3つの単項関数（ f 、 g 、 h ）を組み合わせたい場合、どちらを最初に接続してもかまいません。 これは、整数に適用したときに加算と乗算も結合するという事実に類似しています。

これらの法律はあいまいになじみがないように思われませんか？ 対応する「法則」を見てみましょう。これは通常の合成機能によって満たされます。

1 id f == f
2 。 f id == f
３ 。 （ f。g ） 。 h == f 。 （ g。h ）

idは中立要素、ユニットです。 類似点を見つけましたか？ ユニットを左または右に配置した関数を合成すると、同じ関数が再び与えられ、合成関数は結合性になります。 コンポジションのモナド関数は連想的でなければならず、 戻り値は単一の関数のモナド同等物でなければならないので、モナド合成の動作は通常のコンポジションの動作と同様に予測可能です。

プログラマーの観点からこれらの法律の意味は何ですか？ モナドがインテリジェントに動作するようにしたいので、 returnと>> =の定義はこれらの法則を満たさなければなりません。 >> =およびreturnの定義を確認する方法をすぐに学習します。 [モナドの法則は>> =演算子ではなく>>>演算子で表されますが、 >> =を使用してバージョンが表示されることに注意してください。これは同等です。]

ただし 、キャッチがあります：Haskell はモナドの法則をチェックしません ！ チェックされるのは、 戻り値と>> =定義タイプが正しいことだけです。 法律が実施されているかどうかにかかわらず、プログラマは確認する必要があります。

多くの人が「なぜHaskellがモナドの法則をチェックできないのか？」と尋ねます。答えは簡単です：Haskellはまだ強力ではありません！ モナドの法則の正しさを証明する十分に強力な言語を取得するには、定理証明者（定理証明者）のようなものが必要です。 定理の証明は息をのむようなものであり、プログラミングの未来かもしれませんが、従来のプログラミング言語よりもはるかに複雑です。 興味があれば、Coq定理の尊敬される証拠があります 。それはここから入手できます 。 しかし、Haskellでは、プログラマーは、自分が書いたモナドがモナドの法則に違反しないように注意する必要があります。

glyいバージョン

niceバージョンの問題は、 > =>演算子がMonad型クラスで直接定義されていないことです。 代わりに、上で示したように、 >> =演算子が定義され、 > =>演算子が派生します。 したがって、定義を>> >>およびreturn演算子に制限する場合、 returnおよび>> =のみを含むモナド則が必要です。 また、この形式では、前のセクションで示したものよりも直感的ではありませんが、Haskellのモナドに関するほとんどの書籍やドキュメントで提供されています。

>> =演算子と戻り関数に関して、モナドの法則は次のようになります。

1 return x >> = f == f x
2 。 mv >> = return == mv
３ 。 （ mv >> = f ） >> = g == mv >> = （ \ x -> （ f x >> = g ） ）

ここで、異なる値のタイプは次のとおりです。

mv :: m a
f :: a- > m b
g :: b- > m c

いくつかのタイプa 、 b 、 cおよびある種のモナドmに対して 。

素敵なバージョンからモナド則のいバージョンを派生させる

楽しんで、素敵なバージョンからモナド則のいバージョンを推測してみましょう。 計算では、上記で検討したモナド合成の定義が必要です。

f > => g = \ x -> （ f x >> = g ）

法律1：

return > => f == f
\ x -> （ return x >> = f ） == \ x- > f x
return x >> = f == f x -QED（「証明するために必要」）

\ x-> fxは fと同じであることに注意してください。

法律2：

f> => return == f
\ x->（fx >> = return）== \ x-> fx
fx >> = return == fx
let mv == fx
mv >> = return == mv-QED

法律3：

（ f > => g ） > => h == f > => （ g > => h ）
\ x -> （ （ f > => g ） x >> = h ） == \ x -> （ f x >> = （ g > => h ） ）
（ f > => g ） x >> = h == f x >> = （ g > => h ）
（ \ y -> （ f y >> = g ） ） x >> = h == f x >> = （ \ y -> （ g y >> = h ） ）
-計算（\ y->（f y >> = g））x取得：（f x >> = g）
（ f x >> = g ） >> = h == f x >> = （ \ y -> （ g y >> = h ） ）
-mv = f xとし、次に：
（ mv >> = g ） >> = h == mv >> = （ \ y -> （ g y >> = h ） ）
-gをfに、hをgに置き換えます。
（ mv >> = f ） >> = g == mv >> = （ \ y -> （ f y >> = g ） ）
-正しい式でyをxに置き換えて、以下を取得します。
（ mv >> = f ） >> = g == mv >> = （ \ x -> （ f x >> = g ） ） -QED

計算ステップ（\ y->（fy >> = g））xでは、単に関数全体（ \ y-> ... ）を引数xに適用します。 この場合、 yは関数本体の変数xに置き換えられ（省略記号（...）で示されます）、関数本体が結果として返されます。 Lingo関数型プログラミング言語では、この操作はベータ削減と呼ばれます。 {1：この場合、我々はラムダ計算と呼ばれる数学のセクションについて話している。これは、とりわけベータ削減を記述している。}ベータ削減は、関数を計算する主な方法である。 次の2つの関数が正しいため、 yがxで置き換えられる最後のステップは正しいです。

\ x- > f x
\ y- > f y

-これはまったく同じです（正式な引数の名前は重要ではありません）。 Lingo関数型言語では、2つの関数はアルファ版と同等です。 他の手順を理解している必要があります。

アイデアは何ですか？

モナドの法則は、コードで時々使用され、長い式を短い式に置き換えます（たとえば、 return x >> = fの代わりに、単にfxを書くことができます）。 ただし、次の記事では、モナドの法則の主な利点は、特定のモナドのリターンと>> =の定義を導出できることです。

この記事の最後で、きちんとした構文形式の記述を示したいと思います。その助けを借りて、モナドのコードがより良く見えるようになります。

抽象的

上記で定義したreadAndPrintLineTwice関数を思い出してください。

readAndPrintLineTwice :: IO （ ）
readAndPrintLineTwice = getLine >> = \ s- > putStrLn s >> putStrLn s

彼女には1つの利点があります：それは1行で書かれています。 欠点は、世界で最も読みやすい行ではありません。 Haskellの設計者は、モナド定義を読むのが難しいことが多いことに気付き、定義を読みやすくする本当に素晴らしい構文糖を見つけました。

この構文糖の基礎は、モナドコードの膨大な数の操作が2つの形式で記述されているという観察です。

-フォーム1。
-mv :: m a
-f :: a-> m b

mv >> = \ x- > mf x

-フォーム2。
-mv :: m a
-mv2 :: m b

mv >> mv2

表記法は、これらの2つの形式を読みやすくすることを目的として設計されました。 doキーワードで始まり、その後にいくつかの単項演算が続きます。 したがって、これらの2つの例はdo表記で記述されます 。

-フォーム1、表記法。
do v < -mv
f v

-フォーム2、表記法。
MVを行う
mv2

フォーム1の最初の行は、モナド値mvを取得し、それをvと呼ばれる通常の値に「アンパック」することを意味します。 2行目はvからfを計算しているだけです。 文字列fvの結果は、式全体の結果です。

フォーム2では、最初の行でモナド値（「アクション」） mvが 「実行」されます。 2行目は、別のモナド値（「アクション」） mv2を 「実行」します。 したがって、 >>演算子のように、 mvとmv2をシーケンスに連結する表記法があります。

Haskellコンパイラは、便利なdo表記をForm 1およびForm 2の非doエントリに変換します。これは単なる構文変換であり、両方のエントリの意味は同じです。 さらに、両方の形式を各表記法の1つの表現に混在させることができます。 例：

-mv :: m a
-v1 :: a
-f :: a-> m b
-v2 :: b
-mv3 :: m c

する
v1 < -mv
v2 < -f v1
mv3
v2を返す

これはまったく同じです：

mv >> = （ \ v1- >
（ f v1 >> = （ \ v2- >
（ mv3 >>
（ v2を返す ） ） ） ） ））

またはskokbokなし：

mv >> = \ v1- >
f v1 >> = \ v2- >
mv3 >> v2を返す

モナド式が大きくなっても、 do- formは読みやすく、 doなし（ "Sugared"とも呼ばれる）のフォームは読みにくくなることがよくあります。 それが、 do- abstractが存在する理由です。 do- abstractは、1つだけでなく、 すべてのモナドで機能するのは素晴らしいことです。

さらに、 do表記とシュガーレス表記を1つの式に混在させることができます。 このように：

do v1 < -mv
v2 < -f v1
mv3 >> v2を返す

これは便利な場合もありますが、コードの可読性が低下することがよくあります。

前の例がdo記法でどのように見えるか見てみましょう。

-行を読んでから印刷します。
readAndPrintLine :: IO （ ）
readAndPrintLine =
する
行< -getLine
putStrLn行

-2行ずつ印刷します。
-機能ではありません。
する
putStrLn 「これはストリング1です。」
putStrLn 「これは文字列2です。」

-行を読み、2回印刷します。
readAndPrintLineTwice :: IO （ ）
readAndPrintLineTwice =
する
行< -getLine
putStrLn行
putStrLn行

ここでは、コードはdo -notationのおかげで読みやすくなっています。 興味深いことに、これには追加の利点（または、保持するビューに応じて不利な点）があります。Haskellのコードは必須に見えます！ コードを上から下に読むと、矢印<-を割り当てる代わりに命令型言語のように見えます。 readAndPrintLineは次のように記述できるとしましょう。「 getLineを呼び出して、 行変数に入れた行を読み取ります。 次に、 putStrLnを呼び出してこの変数を出力します。」これは、実際には実際には起こりません（たとえば、 行は変数ではありません）が、そのように読むことができます。 多くの入出力を行う多くのコードでは、 do- abstractは非常に便利な記述方法です。

表記には他の有用なプロパティがあります。 たとえば、 do表記の本文にlet式とcase式を埋め込むことができます。これはしばしば便利です。 これはルーチンであるため、詳細には触れません。他のHaskellチュートリアルを使用して、この点を調べてください。

次回

次の記事では、 Maybe （エラーが発生する可能性のある計算のモナド）から始まり、リストモナド（複数の結果を伴う計算の場合）で終わるモナドについて説明します。

内容

パート1：基本
パート2：関数>> =およびreturn
パート3：モナドの法則
パート4：多分モナドとリストモナド