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

dif_engine @dif_engine

ゲンツェンのハウプトザッツ、大学一年のときに頑張って証明を読んだ。読んだんだ…。理解できなかったけど…。理解した気がしないというか理解とは何なのかとかもう

dif_engine @dif_engine

「「証明とは何か」ということについての証明」とはなんだろうか？「「証明とは何か」ということについての証明」についての推論規則として何が許容されるべきだろうか？　果たして私はまだ正気なのだろうか？　←　色相が濁り始めてる。もうすぐ執行対象。#PSYCHOPASS #アニメ

dif_engine @dif_engine

圏論が教えてくれる「デザインの良さ」というのは例えば「（型についての）パラメトリック多相な関数は自然変換にするといいよ」ということなのだけど、その「いいよ」感をそれだけ取り出して伝えることは難しい、というか多分ムリ。

みょん @myuon_myon

@dif_engine ただ「自然変換にするといいよ」って言ってもnaturalityをコードに表現できない言語ではあんまり(圏論的によく分かる以上の)意味が無かったりしますよね

dif_engine @dif_engine

@myuon_myon 自然性をダイレクトに記述できないのはたしかに残念です。自然性を表す可換図式からRULESの中の書き換え規則を（プログラマが自分の手で）書くなんてことには一応使えるかもしれない（期待）。

みょん @myuon_myon

@dif_engine なるほど、将来的にそういう応用につながる可能性はありますね

dif_engine @dif_engine

@myuon_myon PreludeのFunctorにも RULES 沢山入ってますが、ああいうのを頑張って自分で書くためにはコンパイラの中のことをキチンと把握してないとダメだろうなぁと思います。

dif_engine @dif_engine

沢山、でもないか

みょん @myuon_myon

@dif_engine パフォーマンス向上のためには泥臭いことがついてまわるのは仕方ないですね。個人的にそのへん触りたくないので誰かがやってくれるといいなーっていう立場です。