book
归档: Haskell 
flag
mode_edit

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

同构(Isomorphism)

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

所以我们如果要证明两个类型 a, b 同构,只需要实现 a -> bb -> 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 xsRight () ,注意到右边实际上只有 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)
navigate_next