0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

アプリカティヴとしての函数型構築子

Last updated at Posted at 2013-12-08

相変わらず函数型コンストラクタ (->)

次に函数型コンストラクタがアプリカティヴ(なファンクター)であることを確認していく。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<*>gf<$>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のデータのフォルダがあるわけだ。

それはともかく、(->)アプリカティヴに<$>とか<*>とかのアプリカティヴ・スタイルを使えると何が面白いのかを試してみるのはまたこんど。

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?