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

朝風呂に入っていたら頭に浮かんだ、ものすごく素朴な疑問。
整数なり実数では普通に $x \times x = x ^ 2$ だけど、カルテシアン閉圏 (CCC) 一般に、任意の対象 $A$ で $A \times A \simeq A ^ 2$ なのだろうか？普通にそうなりそうだし、集合の圏ならすぐ証明できそうだけど。
つか、普通の（型付）関数型言語でどうだろう？としばし考えてみる。基本は、 $f : A \times A \to A^2$ と $g : A ^ 2 \to A \times A$ で、かつ $g \circ f$ と $f \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の日記

ソフトウェア工学系研究者 → AIエンジニア → スクラムマスター・アジャイルコーチ

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