bonotakeの日記

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

関数型言語で x × x = x ² を示す

朝風呂に入っていたら頭に浮かんだ、ものすごく素朴な疑問。
整数なり実数では普通に x \times x = x ^ 2 だけど、カルテシアン閉圏 (CCC) 一般に、任意の対象 AA \times A \simeq A ^ 2 なのだろうか?普通にそうなりそうだし、集合の圏ならすぐ証明できそうだけど。
つか、普通の(型付)関数型言語でどうだろう?としばし考えてみる。基本は、  f : A \times A \to A^2  g : A ^ 2 \to A \times A で、かつ  g \circ ff \circ g がそれぞれ恒等射になるような  f, g があればよい。*1
ということで、Haskellでそういう  f, g を書いてみた。A \times A はタプルで*2 2はBool型で*3解釈している。

f :: (a, a) -> (Bool -> a)
f (a1, a2) = \b ->
                case b of
                    True -> a1
                    False -> a2

g :: (Bool -> a) -> (a, a)
g h = (h True, h False)

QuickCheckしてみた。

prop_gf x y = (g.f) (x, y) == (x, y)
 where types = (x :: Int, y :: Int)

prop_fg h x = (f.g) h x == h x
 where types = h :: Bool -> Int
*Main> quickCheck prop_gf
OK, passed 100 tests.
*Main> quickCheck prop_fg
OK, passed 100 tests.

ちゃんとなってるっぽい。
考えてみると、(a, a)型 と (Bool -> a)型 は isomorphic ということか。ふーん。


…とここまで書いたところで、嫁さんに「何してんの」と聞かれたので説明したら「は? x \times x = x ^ 2? 当たり前じゃん」と鼻で笑われたスイマセン

*1:なんでここのtexは \tt を解釈してくれないんだろう…

*2:タプルと圏論の直積が完全にイコールではないと言う話はこちら

*3:本当は Either () 型 でやるのが筋な気がする。

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