bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

unitとvoid

unitは×の単位元(1)で、voidは+の単位元(0)

おーそうだったのかぁ、と思いつつ、ふと疑問が。… void \times X(Xは任意の型) はどうなるのでしょう?
状況からして、直積、直和があってそれぞれに単位元1、0があるような圏を考える訳ですよね。

こっからは当て推量ですけど、strictな言語なら f(\perp \times A) = \perpとなって欲しいと思うので、直感的には 0 \times X \simeq 0  (\simeqは同型)となりそうな気がするんだけれど、これってつまり、distributive law が成り立つと言う状況で。
でも、確かこないだの圏論勉強会で「MLのようなstrictな言語の圏ではdistributive lawは成り立たない」みたいな話をしてた気が*1。…あや?違うのかなぁ。謎。


※いつものごとく豪快に勘違いをしている可能性大アリなので、そんときゃ許してくださいませ。

*1:うろ覚えなので正確さを欠いているかもしれません。というか多分不正確。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。