Haskell の "(>>=) Just" の型の意味を教えてください

Question

前提

私は Haskell を学習し始めたところで、根本的なところに気付いておらず、それでおかしな質問をしているのかもしれませんが、どうぞ宜しくお願い致します。

実現したいこと

Haskell で (>>=) Just の型を調べようとしたら、以下のようになりました。しかし、その意味を読み取ることができず行き詰まっています。
初学者の質問で大変すみませんが、ご教示くださると大変ありがたいです。

:type (>>=) Just
(>>=) Just :: (Maybe a -> a -> b) -> a -> b

試したこと

(>>=) Just の意味を読み取ろうとして、以下のように試したのですが、やはり行き詰まってしまいました。
最初の２つはそうなるのだろうな、とは想像できたのですが、最後の２つが理解できていません。
(>>=) Just に pure :: a -> f a を適用すると、なぜ a -> Maybe a になるのでしょうか？

Just 5 >>= pure
Just 5

Just 5 >>= Just
Just 5

:type Just >>= pure
Just >>= pure :: a -> Maybe a

:type Just >>= Just
エラーが表示されました。

Answer 1

こんにちは。

意図せず関数モナドのインスタンスを利用していることで混乱しているようですね。
実はモナドの m には (->) x を入れる事ができ、m a は x -> a となることができるのです。

質問の例について、型を順番に追いかけてみましょう。
(>>=) の型は m a -> (a -> m b) -> m b で、これに Just :: x -> Maybe x を適用するわけなので、まずは m a に x -> Maybe xを当てはめることを考えます。
とすれば、このとき a は Maybe xに、m は (->) x になるわけですね。
これを (>>=) の残りの型に当てはめると、(a -> m b) は (Maybe x -> (x -> b))、m b は (x -> b) になります。
というわけで、(>>=) Just の型は (Maybe x -> x -> b) -> x -> bであり、 x を a に読み替えれば質問に書かれた型になるわけです。

これにさらに pure :: a -> f a を適用することを考えます。
(Maybe x -> x -> b) に当てはめるには、a は Maybe x となり、f は (->) x なので、pure は (Maybe x -> x -> Maybe x) となります。
これにより、(>>=) Just の b は Maybe x であることがわかるので、最終的に (>>=) Just pure の型は x -> Maybe x に決定します。

Comments

[KN2018]

とても丁寧に教えてくださり、ほんとうにありがとうございます！インターネットで自分なりに調べていたのですが、Haskell は記号が多いために情報の検索が難しく、何時間も行き詰まっていたので、大変に深く助かりました。教えて下さったことをもとに、以下のように考えてみました。もし、お時間が許すようでしたら、読んでくださるととてもありがたいです。

(>>=) Just
= (m a -> (a -> m b) -> m b) (x -> Maybe x)

(x -> Maybe x) が (m a) に一致するように解釈されるため、
m = (->) x, a = Maybe x と解釈され、

= (Maybe x -> (x -> b)) -> (x -> b)
= (Maybe x -> x -> b) -> x -> b (∵ -> は右結合)

上式に、pure :: a -> f a を適応させると

((Maybe x -> x -> b) -> x -> b) (y -> f y)

(y -> f y) が (Maybe x -> x -> b) と解釈されるため、
y = Maybe x, f = (->) x, y = b と解釈され、
(f は Applicative であるため、f は (->) x と解釈させることができる？) ...(ア)

= x -> b
= x -> Maybe x

---
Just >>= Just
= ((Maybe x -> x -> b) -> x -> b) (y -> Maybe y)

(y -> Maybe y) が (Maybe x -> x -> b) と解釈されるため、
y = Maybe x は良いが、Maybe y が (x -> b) と解釈できないためエラー ...(イ)

以上のように考えたのですが、(ア) と (イ) の部分に自身が持てていない状態です。

長文になってしまい、大変申し訳ないのですが、上のことが正しいとすれば、(ア) の部分で解釈された f = (->) x の情報はどこにも残らずに捨ててしまわれるのでしょうか？

Just >>= pure の型がうまくとれたため、てっきり pure は (a -> Maybe a) となっているのかとも思っていたのですが、、、。

大変厚かましいお願いで恐縮の至りですが、もし、上記のことにコメントをいただけると、とても嬉しいです。
とても丁寧に教えてくださり、また、時間を掛けて解答を書いてくださって、本当にありがとうございました。

[tamoto]

(ア) と (イ) どちらも完璧に正しい認識です。素晴らしいですね。

「捨ててしまう」という表現についてはちょっと正しく理解できているかわかりませんが、
式 (Just >>= pure) の (>>=) で使われている m は ((->) x) なので、pure は (a -> x -> a) で確定します。
(>>=) の第二引数は (a -> m b) を要求しているので、(pure :: a -> f a) を当てはめる場合は必ず m == f となります。
(Just 5 >>= pure) の (>>=) は Maybe モナドですが、(Just >>= pure) は関数モナドの合成になっているわけですね。

ところで、Just の型を見ると a -> Maybe a となりますが、これは「 f を先に Maybe と確定させた pure 」 と同じように考えることができます。
そうすれば、(>>=) の m が ((->) x) のとき、なぜ pure だと通り Just ではダメなのかが一発でわかると思います。

[KN2018]

大変遅い時間にも関わらず、ご教示をくださり、本当に深く感謝しております！
また、初学者にも関わらず、お褒めの言葉を下さり、大変恐縮しております。褒めていただけるレベルにはまったく達していませんので、今からさらに頑張る所存です。
最初に教えて下さった「関数モナド」という言葉を頼りにいろいろ調べていました。その言葉を教えて下さったおかげで、「Just >>=」を関数モナドとして意識できていなかったことから、「>>=」に適用するときに「m」がなんであるかが分からず行き詰まっていたんだな、ということがよく分かりました。
さきほどまで、まだ霧の中にいる状態だったのですが、もう一度ヒントを下さったおかげでかなり理解が進んだという気持ちがしています！

たしかに、「Just >>=」を見ただけで、第１引数から「m = (->) x」と分かるので、第２引数の関数は、戻り値が「(->) x b」であるものでなければならないと分かる。したがって、Just を適用することはできない、とすぐに分かるのですね。（Just の戻り値は Maybe y で (->) x b になり得ない。）pure であれば、パターンマッチングにより、戻り値を自在に合わせられるから大丈夫なんだろうな、と思っています。
「f を先に Maybe と確定させた pure」というように表現を変えて伝えてくださって、理解が進むきっかけになりました。ありがとうございます！このように言い換えてもらえることが、どれだけありがたいことか、身にしみて今感じています。

Haskell に関しては、分かった気がする！と思っても、やっぱり分かってなかった、みたいなことを繰り返していますので、まだまだあやふやなのですが、努力しようと思っています。
関数モナドの定義はなんとか分かるのですが、それを一体どう活用するのか分からず疲れてきていたところでしたが、丁寧に教えて下さったおかげで、努力する気持ちが湧いてきて、大変嬉しいです。
大変丁寧に教えてくださって、本当にありがとうございました。