Haskellの多相関数と自然変換(というか射の族)について
(Kan拡張のとこ以外)読み終えた。随伴がモナドを伴う、というのは知ってたけど具体的にHaskellコードに落とせるというのは面白い。 / Haskellと随伴 by @myuon_myon on @Qiita http://t.co/AiN2UsRJVX
— xenophobia (@xenophobia__) 2014, 12月 5
そんなことより、多相関数を与えることとHask -> Haskな関手間の自然変換を与えることとがほぼ対応する、という事実に気付かされたので意義深かった。 > アドベントカレンダー4日目記事
— xenophobia (@xenophobia__) 2014, 12月 5
これなんですが、以前も聞いた気がするし*1、忘れないように備忘録をば。
たとえば、HaskellでInt -> Double型の関数を1つ与えるというのは、Hask圏において対象Intから対象Doubleへの射を1つ与えることに対応していると思ってよい。
そういう視点で今度はforall a . a -> [a]型の多相関数を考えてみる。
aにある具体的な型、つまりHaskの対象Xを代入すると一つの具体化された型 X -> [X]が決まり、それに対応してHask圏上の(Xから[X]への)射が1つ与えられることになる。
つまり、forall a . a -> [a]型の多相関数は、Hask圏上の射の族と対応していると考えることができるはず。
射の族が表せるなら、自然変換も表せるという道理になる。*2
つまり、
nat :: (Functor f, Functor g) => f a -> g a nat = ...
という多相関数は、関手から関手への自然変換と対応していると考えることができるし、
nat_l :: Functor f => f a -> a nat_l = ... nat_r :: Functor g => a -> g a nat_r = ...
はそれぞれ自然変換及び自然変換と対応していると考えることができる。
そういう視点でMonadのreturn, joinの型を見ると、
class Monad m where return :: a -> m a join :: m (m a) -> m a
これらはそのまま圏論のモナドの2つの自然変換の成分とに対応しているというのがはっきりわかる。
今までHaskellでのMonadの定義と圏論におけるモナドの定義はなんとなく一致してるなーぐらいの感覚で見ていたんですが、今回この多相関数と自然変換との関係を再確認することでより理解が深まった感じがします。よかったよかった。
ところで、Functorのfmap :: (a -> b) -> f a -> f bも多相関数ですが、あれは関手の射関数を表しています。
したがって、fmapはHask圏の射の族ではなく、射を射に写す関数の族を表していると言うべきでしょう。
Haskellの(->)はHask圏の射であり、かつ関数でもある*3ので、どちらと取ればいいかには常に気をつけていく必要がありそうですね。
*1:http://d.hatena.ne.jp/hiratara/?of=15 を見るにつけおそらく圏論勉強会で既に学んでいるはず。
*2:自然性をコードで表現できると言っている訳ではない。
*3:あと、A -> B(A,Bは具体的な型)はそれ自体が型なのでHask圏の対象でもありうる。