V.S. Hask圏
Hask圏
Haskellをラムダ計算とみなした時のsyntactic categoryをHask圏というのがよく言われる定義である(と思う)。
Haskellのtypeをobject, hom(A,B) をjudgement x:A |- M:B 全体(を適当な同値関係で割ったもの)とみなして圏を作る(このときしばしばjudgementとこのjudgementから作ったfunction λx.M を区別しない)。
さて基本的な結果として次のことが知られている。
というわけでHask圏は圏にならないのでそのようなものは存在しない。
Why not?
これはundefinedというヤバイ元の存在とcall-by-needの悪魔的評価規則が合わさりこのような現象が生み出される。 主にこの2つが悪さをしているので、この辺をどうにかできればHask categoryが作れる可能性がある。
undefinedを抜く
undefinedは「評価ができない(プログラムが正しい値を返さない)」ことを表す元で、普通は(多分)domainのbottomに対応させ、無限ループするプログラムの解釈なんかに使う。 undefinedを抜くためにはプログラムが常に停止して値を返す必要があるので無限ループができないようにする必要がある。
とまぁ言うのは簡単でfixpointを抜けばいいだけなんだけどfixpointもないcalculusがプログラミング言語を名乗るのは片腹痛いのでこれはちょっとナシかなという気持ちになったりする。
call-by-needを捨てる
call-by-needを捨てて、call-by-valueとかcall-by-nameとかそういうやつに行くというのも1つだと思う。 GHCのStrict拡張を入れてライブラリもStrict付けて全てビルドしなおせばそれはもうcall-by-valueになる(よね？)はずだったり、まぁcall-by-nameもcall-by-needみたいなもんやろという乱暴な考え方によりcall-by-needを捨てるのは現実的な案だと個人的には思う。
しかしcall-by-needではないHaskellはそれはもうHaskellなんですか(反語)ということもあるのでアイデンティティを捨てる勇気が必要かもしれない。
ここからポエム
いずれにせよHaskellという純粋関数型プログラミング言語でHask圏を考えるというのは無理があるということが分かるのだけれど、じゃあHask圏についてcomputer science的に意味がないかというと個人的にはそんなことはないと言いたかった。
個人的に、CSとは「計算機で観測可能な現象に説明をつける」学問であると思うので、実際にHaskellという言語で観測可能な現象について圏論で説明をつけようとする営み自体が否定されることはないと思う。 計算機が発明されて間もないからなのか人類が遅れてるのかはわからないけれど今は計算機の説明を付けるために用意した圏論的なモデルが上手くモデルとして機能していない(モデルが現象の構造を反映する力が弱い)のかもしれないけれど、とりあえず数学的にわかりやすいモデルを取ってきていくつかの技術的な難しさ(categoryにならないとかね)を無視した上で似たような現象をシミュレーション出来ないかを調べている段階だと思えばいいんじゃないかなと。
実際にHaskellに限らず色々なプログラミング言語で観測可能な現象について圏論の方からそれっぽいモデルを提供するぜ的研究はあちこちで見られるので、call-by-needとかにも上手い説明を付けられる直観的で構成が大変じゃないモデルを誰か思いついてくれればよいのだけど。
data & codata
HaskellのListがListかつColistであるというのは有名な話だけれど、こういうdatatypeかつcodatatypeがとれるような圏を考えるきっかけは(歴史的なことには私は詳しくないのだけれど)こういうプログラミング言語からの現象が先にあったのかな？と想像してる。 ちなみにこのようなcategoryはalgebraically boundedと呼ばれたりします。
enrichmentの隠蔽
関係ないのだけどHask categoryで圏論やろうとするとenrichmentが色々効いてきて困る、みたいな話をよく聞くし自分もそう思うのだけれど、実はenrichmentは結構避けられる(隠蔽できる)のかもと書いていてちょっと思った。
例えばFunctorのfmap methodは fmap: (Functor F) => (A -> B) -> FA -> FB という形で書かれる。
これはHaskからHask(の適当なsubcategory)へのfunctorのfmapの型になっているが、圏論的には実際は次のような形をしているはずである: fmap: Hask(A,B) -> Hask(FA,FB) .
そしてここでの -> は単なるfunction(写像)、 Hask(A,B) の元に対して Hask(FA,FB) の元を対応させるものである。
これだけ見るとHaskellの定義はfunctionがexponentialに化けているので、実はこのFunctorはHask-enriched functorで、Haskのhomがobjectだからというなんやかんやを考えないといけないのでは、と思うのだけれどそれは一応回避することができる。
最初にも書いたとおりHask categoryはsyntactic categoryで、さらにjudgementとそれからできる関数を区別しないようにする。
すると、 fmap = λf. fmap f はjudgement f:Hask(A,B) |- fmap(f):Hask(FA,FB) とみなせるので普通にfmapと思うことができる。
いやまぁ本質的な部分は全てjudgementと関数を区別しないというところに押し付けられているので何も解決していないのだけれど、ちゃんとenriched category theoryで論をしなくても、 -> とfunctionの読み替えの部分だけできれば多分基本的なcategory theoryはできると思うので、(ほとんどSetと同じやんけと思われる)enrichmentをフルで考えなくてもいいということはかなり負担を軽減してくれる、と思う。
もしかしたらこの同一視を完全にformalizeするとenrichmentが出てくるかもしれないけれど、もしかしたらexponentialとfunctionの同一視(というかinterpretationがあってそれを適切な位置にかけていくだけでいけるみたいな)の部分だけで済むかもしれない？ この辺ちゃんと考えてないのでよくわからない。
おわりに
だいぶポエミーな記事を書いてしまった。