其实这个题在刚刚考完试的时候已经写完了，🕊才知道我为啥能咕到现在。

同构（Isomorphism）

两个类型 a, b 同构，当且仅当存在 a, b 间的双射，即 a, b 等势（一个集合的势可以感性地理解为集合中元素的数目，对于一个类型来说，就是该类型的所有可能取值）。

所以我们如果要证明两个类型 a, b 同构，只需要实现 a -> b 和 b -> a 就好啦。

接着可以证明同构的一些性质：

自反性：

refl :: ISO a a
refl = (id, id)

对称性

symm :: ISO a b -> ISO b a
symm (x, y) = (y, x)

传递性

trans :: ISO a b -> ISO b c -> ISO a c
trans (u, v) (x, y)= (x . u, v . y)

比起前面的无脑凑函数，比较难实现的一点是 isoEU :: ISO (Either [()] ()) (Either [()] Void)

这个可能会比较反直觉：「明显左边势更大嘛，怎么可能同构呢？」

首先考虑从左边射到右边。左边有两种情况：Left xs 和 Right () ，注意到右边实际上只有 Left ys 这一类取值，所以我们得把 Right () 映射成 Left ys。这就相当于，左边是数集 $A={-1,\ 0,\ 1,\ \cdots, \ k,\ \cdots}$ ，右边是数集 $B={0,\ 1,\ 2,\ \cdots,\ k,\ \cdots}$，这样以来，$A\to B$ 的双射就是 $x \mapsto x+1$ ，反过来就是 $x \mapsto x-1$。写成代码的话就是这样：

isoEU :: ISO (Either [()] ()) (Either [()] Void)
isoEU = (f, g)
  where
    f (Left t) = Left (():t) -- bijection
    f (Right ()) = Left []
    g (Left []) = Right ()
    g (Left (_:xs)) = Left xs

代数数据类型

考虑各种内置类型的势：

Void has cardinality of $0$ (we will abbreviate it Void is $0$).

() is $1$.

Bool is $2$.

Maybe a is $1 + a$.

We will be using peano arithmetic so we will write it as S a.

https://en.wikipedia.org/wiki/Peano_axioms

Either a b is $a + b$.

(a, b) is $a \times b$.

a -> b is $b ^ a$. Try counting (() -> Bool) and (Bool -> ())

这样以来，我们就可以证明一些有意思的东西了：

加法交换律

plusComm :: ISO (Either a b) (Either b a)
plusComm = (f, g)
  where
    f (Left a) = Right a
    f (Right b) = Left b
    g (Left b) = Right b
    g (Right a) = Left a

加法结合律

plusAssoc :: ISO (Either (Either a b) c) (Either a (Either b c))
plusAssoc = (f, g)
  where
    f (Left (Left a)) = Left a
    f (Left (Right b)) = Right $ Left b
    f (Right c) = Right $ Right c
    g (Left a) = Left $ Left a
    g (Right (Left b)) = Left $ Right b
    g (Right (Right c)) = Right c

乘法分配律

dist :: ISO (a, (Either b c)) (Either (a, b) (a, c))
dist = (f, g)
  where
    f (a, Left b) = Left (a, b)
    f (a, Right c) = Right (a, c)
    g (Left (a, b)) = (a, Left b)
    g (Right (a, c)) = (a, Right c)