関数ファンクターにセットされる型の実体について

Question

今更ですが、Haskellを始め、未知の世界の楽しさにハマっています。

そんなところ、関数モナドが今ひとつ飲み込めず、もやもやしています。

関数モナド（Readerモナドとも呼ぶようですね）のバインドの定義と実装は、

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

  h >>= f = \w -> f (h w) w

となっています。

ざっくりとした解釈では、hにm a に当たる、関数ファンクターの値（単引数の関数、例えば(+3)など）がセットされると思うのですが、この場合、mには((->) r)が対応することになります。ここでのaの実体はなんなのでしょうか？

Maybeファンクターなどは、Just 3のように、aに当たるものが明確なのでわかりやすいのですが、単引数の関数から、何を読み取ればaになるのかわからないのが、もやもやの原因です。

以上、ご回答いただければ、ありがたいです。

Answer 1

一言で言うと、aは「関数の戻り値」です。

((->) r)は(+ 3)のように、関数型を表す演算子->の左辺（第1型引数）にrという型変数を適用したものを表しています。
->の左辺は関数の引数の型を表していて、もう一つの引数である右辺は関数の戻り値の型を表しているのでした。
なので、例えば((->) r a)という型はr -> aと等価で、「rを受け取ってaを返す関数」を表していますし、((->) Int Bool)という型はInt -> Boolと等価で「Intを受け取ってBoolを返す関数」を表しています。

従って、((->) r)は「->に対して、引数の型rのみを適用した型」であり、それをMonadやFunctorにおけるmやfとして扱うと、m aは((->) r a)、すなわち「rを受け取ってaを返す関数」と置き換えられることになります。
つまりaはやっぱり「戻り値の型」なんですね。

やや長くなったので一旦割愛しますが、h >>= f = \w -> f (h w) wという(>>=)の実装における各式の型を詳細に見ても、関数モナドにおけるm aのaが関数の戻り値となっていることがわかるはずです。

ちなみに、((->) r a)がr -> aと等価であることを確かめるには、GHCiに下記のように入力して、idなど適当な関数に対して((->) a a)という型注釈を付けてみるといいでしょう。

> :t id :: ((->) a a)
id :: ((->) a a) :: a -> a

さらに、敢えて間違った型注釈を付けてみると、((->) a b)という表記が関数型として認識されているのがよくわかるかと思います。

> :t id :: ((->) a b)

<interactive>:1:1: error:
    • Couldn't match type ‘a1’ with ‘b1’
      ‘a1’ is a rigid type variable bound by
        an expression type signature:
          forall a1 b1. a1 -> b1
        at <interactive>:1:7-16
      ‘b1’ is a rigid type variable bound by
        an expression type signature:
          forall a1 b1. a1 -> b1
        at <interactive>:1:7-16
      Expected type: a1 -> b1
        Actual type: b1 -> b1
    • In the expression: id :: ((->) a b)

Comments

[Meganezaru]

丁寧なご回答、ありがとうございます！

すごくわかりやすい説明で助かりました。
現時点では、もやもやがすっきりと晴れた気がしています。

（今まで、わかった！あれ違うかも・・・そういうことか！やっぱり違う・・・を繰り返してきたので、予断を許しませんが・・・笑）

今までは、形としてなんとなく理解しつつも、(+ 3)の、3（Just 3の、3と同じものに見えてしまう）に引きずられていたようです。

この場合は、3から推論されるNum型が、aの実体になるというイメージで理解はあっていますか？
バインドの結果、出来上がる関数に渡される引数wの型と、m aに当たる関数の引数の型が同じにならなければならないと分かる、という感じでしょうか？

型注釈の確認も参考になります。
手段が一つ増えたので、理解が進みそうです。

とにかく、前に進めそうな雰囲気になりました！
ありがとうございました！

[igrep]

> この場合は、3から推論されるNum型が、aの実体になるというイメージで理解はあっていますか？

はい、正確には、3から推論される「Num型クラスのとある型」が+の第1引数なので、戻り値と引数の型がすべて一致している、という+の型宣言から、「Num型クラスのとある型」がm aのaの実態になるということです。

[Meganezaru]

はっきりイメージが湧きました！
ありがとうございました！