haskell-jp / math #11 at 2021-12-10 23:39:20 +0900

今ちょっと気になったのですが、Haskellの型と関数の「圏」Hask って、
f: a → b, g: b → c に対して、

f >>> g =  f `seq` g `seq` \x -> g (f x)

で定義すると本物の圏ですか？

https://stackoverflow.com/questions/48485660/is-hask-even-a-category なんかそのものずばりの話をしているように見えるページをみつけたのですが、内容はよくわかっていません^^;

undefined と seq の組み合わせめんどくさいねという話と、「そもそもこの圏において射が等しいとはどう定義すべきか」という話が出ているように見えますね

ただ、一つ疑問なのですが、この例でいうところの undef1 と undef2 は等しいのか等しくないのかという以前に、そもそもこれらは「射」なのでしょうか？　この圏では「型」を対象とするのでこの圏における射は monomorphic な関数のみだと思うのですが、 undef1 や undef2 は polymorphic なのでそもそも単一の射ではない気がするのです（あえていうなら自然変換でしょうか？）

問題ありません、と言いそうになりましたが、正確には定義によります。a, b が型である時に、Hom(a,b) は a -> b に instantiateできる式の全体に適切な同値関係を入れたもの、とすれば射になるし、Hom(a,b) は a -> b に型推論される式の全体に適切な同値関係を入れたもの、とするなら射にはなりません。後者とするなら undefined :: a -> b とか (\x -> undefined) :: a -> b を考える必要がありますね。

この同値関係をうまく入れないと結合律やら単位律が成り立たないわけですが。

この問題なんですが、タプルを正格にするとモノイド圏にならないのが非常にネックなんですよね