2014年末、Hakellや圏論の会話やつぶやき

ちゅーん @its_out_of_tune

自然変換という概念を自然変換という言葉を使わずに表現したい。

dif_engine @dif_engine

@its_out_of_tune 関数型言語前提で言うなら、自然変換というのは「まともな合成関係を満たすような多相関数」です。さっきの「ジェネリックな射」とほとんど同じことですが。

ちゅーん @its_out_of_tune

@dif_engine 「まともな合成関係を満たす」というのをもうちょっとｋｗｓｋ

dif_engine @dif_engine

@its_out_of_tune F, G が Functor のインスタンスとします。このとき n :: F a -> F a という多相関数は f :: X -> Yについて n . (fmap f) = (fmap f) . n となるように振る舞うのが「まとも」です

ちゅーん @its_out_of_tune

型レベルで言えば f a -> g aが自然変換なんだが、なんかこう、もうちょっと雰囲気的な事を良い感じに・・・。

ちゅーん @its_out_of_tune

あー、違う、なんで悩んでるのかと言うと、ちゃんと自然変換を説明してしまうと、return :: 1 ~> m という自然変換の1を説明しなくてはいけなくなってしまってすごく辛いんだ。

みょん @myuon_myon

@its_out_of_tune その1は自然変換じゃなくて関手ですよね

ちゅーん @its_out_of_tune

@myuon_myon 区切り位置・・・(´・ω・`)

dif_engine @dif_engine

@its_out_of_tune ああ、恒等関手を「１」で表すのですね。

dif_engine @dif_engine

@its_out_of_tune これだけが、そしてこれだけで「まとも」とも言いがたいのですが、このようなことが成り立っていれば、多くの場合自然な感じであり、多くの場面でなんとなく期待したい性質であるという意味で「まとも」であり、「自然」であるということです。

dif_engine @dif_engine

@its_out_of_tune 具体例として、 n :: Maybe a -> [a] のような多相関数を「皆が期待するように、自然に」実装すると Maybe関手 から List関手 への自然変換になります。

ちゅーん @its_out_of_tune

@dif_engine （すんません、こういう問題だったのです・・・ twitter.com/its_out_of_tun…

ちゅーん @its_out_of_tune

色々悩んだけど、やっぱりId a ≡ a の説明をしてしまうのが楽だし誤解が無さそうだ。

ちゅーん @its_out_of_tune

@dif_engine そうです。けっきょくHaskell上でId a と a が同型である事を軽く説明した上で、「まとも」な f a -> g a が自然変換であると説明するのが一番誤解が無いかなぁという結論に落ち着きました。

dif_engine @dif_engine

@its_out_of_tune はい、恒等関手の説明を（初心者むけには）ちょっと強調するぐらいじゃないと、 a -> F a や F a -> a のタイプの多相関数が自然変換になり得ないという誤解を与えてしまうと思います。

みょん @myuon_myon

Haskellのlensの使い方 (詳しめ) - みゆっきのにっき solorab.net/blog/2014/12/1… いい感じにまとまってる

ちゅーん @its_out_of_tune

@dif_engine ですね。自分の場合、そのせいでずっとreturnが自然変換だというのが納得いかなくてもにょもにょしてたんですよ(´・ω・`)だから逆に「難しい概念だ」とか勝手に思い込んでて避けようとしてたのが冷静に考えたらダメじゃんって話でした。

dif_engine @dif_engine

@its_out_of_tune 「まったく同じ」というほどでもないのですが、結局多項式の一般項で定数項に X^0 を付けて表したりするのと近い精神なんですよ。a X^2 + b X + c = a X^2 + b X^1 + c X^0 みたいに。

ちゅーん @its_out_of_tune

@dif_engine ですね。そういう感覚はこの半年くらいでようやく掴めるようになりました(´・ω・`)ようやく圏論勉強会の中盤くらいででやった事が身になり始めてる感じですぽよ・・・

dif_engine @dif_engine

難波莞爾センセが書いてる、型記号の圏の話おもしろいし、型理論のピュアな形が見て取れて良いのでは感あるけどこれは難波センセの独創なのかしら。

dif_engine @dif_engine

何をもってピュアな形とかいうと色々突っ込みどころがありますが、要するに、全てのデータに「型情報」というタグを付けて管理しましょう、ぐらいの漠然としたアイデアの段階の話です。

dif_engine @dif_engine

「次の曲は Daniel Kan さんの『圏は勝つ』です」

dif_engine @dif_engine

「佳織」をさり気なく「住職」って誤字るのはいくらなんでも卑怯

dif_engine @dif_engine

MacLaneのCWMだって例がいちいち高尚だったりする難しさは今でも感じるのだけど、それを除いて、つまり判るとこだけ拾って読めばそう難しい書き方はしてないと思う。全部はまだ読んでないけど。だけど学部生の時には自然変換のあたりまですら読めなかった。

dif_engine @dif_engine

学部生のときから今までに何か劇的に自分の知識や理解が深まったというならともかく、自分は「すごく出来る」人ではないのでその間も微積や線型代数の復習だとか学部の代数の復習しかしてないんだよなぁ。「わかる」と「わからない」の間には何があるんだろう？