claustrophobia

一般λがなんか書くとか

Haskellの多相関数と自然変換(というか射の族)について

これなんですが、以前も聞いた気がするし*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圏上の射の族{\theta_X: X \rightarrow List(X)}と対応していると考えることができるはず。

射の族が表せるなら、自然変換も表せるという道理になる。*2
つまり、

nat :: (Functor f, Functor g) => f a -> g a
nat = ...

という多相関数は、関手{F:Hask \rightarrow Hask}から関手{G:Hask \rightarrow Hask}への自然変換{\theta: F \Rightarrow G}と対応していると考えることができるし、

nat_l :: Functor f => f a -> a
nat_l = ...

nat_r :: Functor g => a -> g a
nat_r = ...

はそれぞれ自然変換{\theta: F \Rightarrow 1_{Hask}}及び自然変換{\theta: 1_{Hask} \Rightarrow G}と対応していると考えることができる。

そういう視点でMonadのreturn, joinの型を見ると、

class Monad m where
  return :: a -> m a
  join :: m (m a) -> m a

これらはそのまま圏論モナド{(T: C \rightarrow C, \mu, \eta)}の2つの自然変換の成分{\mu: 1_C \Rightarrow T}{\eta: T^2 \Rightarrow T}に対応しているというのがはっきりわかる。

今までHaskellでのMonadの定義と圏論におけるモナドの定義はなんとなく一致してるなーぐらいの感覚で見ていたんですが、今回この多相関数と自然変換との関係を再確認することでより理解が深まった感じがします。よかったよかった。


ところで、Functorのfmap :: (a -> b) -> f a -> f bも多相関数ですが、あれは関手{F}の射関数{F_{Arr(X, Y)}}を表しています。
したがって、fmapはHask圏の射の族ではなく、射{X \rightarrow Y}を射{FX \rightarrow FY}に写す関数の族を表していると言うべきでしょう。
Haskellの(->)はHask圏の射であり、かつ関数でもある*3ので、どちらと取ればいいかには常に気をつけていく必要がありそうですね。

*1:http://d.hatena.ne.jp/hiratara/?of=15 を見るにつけおそらく圏論勉強会で既に学んでいるはず。

*2:自然性をコードで表現できると言っている訳ではない。

*3:あと、A -> B(A,Bは具体的な型)はそれ自体が型なのでHask圏の対象でもありうる。