- 70 名前：デフォルトの名無しさん mailto:sage [2014/03/02(日) 18:17:07.03 ]
- >>69
背景：
例えばHaskellにおける型（具体型），IntだとかFloatだとかがあったとき，
これらの型情報をうまく扱うためには結局「型＝集合」という見方を超えて
「全ての要素にタグ（要するに型情報）がついた世界」を考えたほうが言語の実情に合う．
このような事は実は随分昔にラッセルが創始したタイプ理論というもので行われており，
その当時の動機としては集合論にまつわるパラドックスを回避するとかそんな意味合いが
あったしその理論の完成度も極めて低く今日ラッセルが作った通りのタイプ理論は
まあ普通は使わないんだけど，とにかく「タグが整合性を持って付けられる世界」というのを
集合論と同じぐらいの豊かさで作れる．（いろんな定式がある．）
ここで圏論が出てくる舞台が出来た．「具体的な基礎型」を対象とし，これらの対象を結ぶ射として単相関数を考える
ことにして圏を考える．Haskellで考えるときの名前はHaskと呼ばれる．
簡単な具体例への言及：
そして，Intからリスト [Int] を作る手続きは，圏論的には「Haskから自身への自己関手」として
定式化できる．モナドも自己関手の一種として，圏論的に定式化できるというか元々モナドは
圏論用語ですね．
実際には帰納的に構成されるタイプの型を考えるとHaskellでは「下から上」と「上から下」を
（おそらくは意図して）混同しているので圏論の議論がシャープすぎるところがあるけど，
各種の，例えばFunctor則だとかモナド則だとかはすべて圏論的な図式の可換性条件として
理解できる．
歴史：
Moggiの computational lambda-calculus and monads (1988) なんていう論文
（ネットに転がってる）あたりから出てきた流れだと思われる
|
 |
