sirkerf
連投申し訳ありません。高次元圏をHaskellで実現することはできますか？
3-cellなどの実装もできるのでしょうか。
3-cellなどの実装もできるのでしょうか。
x,y :: Ob に対して f,g :: Hom1 x y, theta :: Hom2 x y f g とかできて欲しいとこで、Haskellは dependently typed じゃないから、自然には Ob = * = Type = TYPE 'LiftedRep になっちゃうし、 Hom1 x y が何かの型になっちゃうんですよね。そうすると Hom2 x y f g の f g にどうやってはめ込むんだって話になるので、ちょっと難しい気がします。`TypeInType` 拡張とか使って data Ob = <hogehoge> とやり data Hom1 x y = <hogehoge> とやって両方kindとみなすなら何とかなりますが、それって Ob も Hom も列挙型くらいにしかならなくてそんなに豊かではない気がしますね…。typeってコンパイル時には消去されるから実行時には2-cellしかいないし。Ob, Mor1, Mor2, Mor3 型を用意し、 id0 :: Ob -> Mor1 , dom1, cod1 :: Mor1 -> Ob 等を用意する。 ただしこうすると comp1 :: Mor1 -> Mor1 -> Maybe Mor1 になって結合の際の dom と cod が一致してないのを実行時エラーとしてしか報告できなくなりますね…。