相変わらず函数型コンストラクタ (->)
次に函数型コンストラクタがアプリカティヴ(なファンクター)であることを確認していく。Applicative型クラスのインスタンスになるためには2つの函数:
pure :: b -> f b
(<*>) :: f (b ->c) -> (f b -> f c)
が必要なわけだ。Functorの時と同様にf = ((->) a)
を考えれば、
pure :: b -> (a->b)
(<*>) :: a -> (b->c) -> ((a->b) -> (a->c))
である。pure
の方は、b型の値をa->b型にする恣意的でないやり方なんかあるのか、という感じだが、要はどんなa型の値が来ようとそれを無視して当のb型の値を返すようにすればいい。というわけで、
pure x = (\_ -> x)
(<*>) f g = \x -> f x (g x)
という定義であるらしい。fmap
(アプリカティヴでは代わりに普通<$>
を使うけれど)はpure f<*>g
はf<$>g
でなければならないので、まずそれを確認しよう:
pure f <*> g = fmap f g
函数ファンクターのfmap
は函数合成(.)
だったから右辺は単にf . g
である。問題は左辺。(<*>) (pure f) g
= \x -> (pure f x) (g x)
だが、(pure f)
はどんな引数がこようがf
を返す函数なのだから(pure f x) = f
である(x
は見事に無視される)。というわけで\x -> f (g x)
になり、これはx
を取ってそれにg
を作用させて更にf
を作用させる函数なわけだから、函数合成f . g
そのものだ。というわけでfmap
に関する規則は成立している。
次は identity 則で:
pure id <*> g = g
というものだ。fmap
に書き換えてやればfmap id g = g
を示せばいいわけ。もちろんファンクター則の第1則からfmap id g = id g
なんだからid g = g
である以上、これは文句なく成立する。
次は composition 則で:
pure (.) <*> f <*> g <*> h = f <*> (g <*> h)
というもの。左辺を考えてやるとまず(.)
とf
を合成(.).f
したものをg
に作用させて\x -> ((.).f) x (g x)
=> \x -> (f x).(g x)
でこれをh
に作用させると \y -> (\x -> (f x).(g x)) y (h y)
=> \y -> (f y).(g y).(h y)
である。 右辺は、まず括弧の中から\x -> g x (h x)
で、これにf<*>
を作用させて、\y -> f y ((\x -> g x (h x)) y)
=> \y -> f y (g y (h y)))
というわけである。これはまさに\y ->(f y).(g y).(h y)
なので、きちんと左辺と一致する。
次が homomorphism則 で
pure f <*> pure g = pure (f g)
左辺は f<$>(pure g) = f . (\x -> g)
だから、どんな引数が来てもそれを無視して結局f g
を返す函数だ。右辺は(\x -> f g)
だからまさに左辺と一致する。
最後が interchange 則で
f <*> pure g = pure (\x -> x g)<*>f
である。左辺は\x -> f x (pure g x) => \x-> f x g
である。右辺は要するにfmap
なので($g) . f
で、引数にf
を作用させたあとに、それをg
に作用させる。これはまさに\x -> f x g
がやっていることだ。というわけで、この法則も成立している。
かくして(->)がアプリカティヴ則をきちんと満足するきちんとしたアプリカティヴであることは証明された。が、そもそもなんでこれらの規則が要求される必要があるのかがまだわかってない。モナドとファンクターの間の強さをこれらの規則が表現してるんだとは思うんだけど、なんでこれらなのかっていう点に関するなんか直観的な説明ってないんだろうか。というか、こんなごくごく単純な例でも面倒くさいのに、他のアプリカティヴやらモナドやらってこんな法則きちんと証明してるのかな、と思ったら、どうもcoqとかの定理証明支援系を使って確認してからHaskellに落としこんだりしてるのか。道理で、Git-Hubとか見てるとcoqのデータのフォルダがあるわけだ。
それはともかく、(->)
アプリカティヴに<$>
とか<*>
とかのアプリカティヴ・スタイルを使えると何が面白いのかを試してみるのはまたこんど。