haskell - 为什么在代数数据类型中，如果我可以为两种类型定义一个特殊的 `from` 和 `to` 函数，这两种类型就可以认为是相等的？

Question

我正在阅读此博客:http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/

它说:

However, when I talk about equality, I don’t mean Haskell equality, in the sense of the (==) function. Instead, I mean that the two types are in one-to-one correspondence – that is, when I say that two types a and b are equal, I mean that you could write two functions

    from :: a -> b
    to   :: b -> a

that pair up values of a with values of b, so that the following equations always hold (here the == is genuine, Haskell-flavored equality):

    to (from a) == a
    from (to b) == b

后来，有很多基于这个定义的法律:

Add Void a === a
Add a b === Add b a
Mul Void a === Void
Mul () a === a
Mul a b === Mul b a

我不明白为什么我们可以根据“平等”的定义安全地得到这些定律？可以使用其他定义吗？我们可以用这个定义做什么？它对 Haskell 类型系统有意义吗？

Answer 1

为了不“提及范畴论或高等数学”，作者绕开的术语是基数。他将两种类型定义为 === - 如果它们具有相同的基数，则它们彼此相等——也就是说，如果一种类型的可能值与另一种的可能值一样多。

因为如果两个类型具有相等的基数，则它们之间存在同构。 Mul () Bool 可能是与 Bool 不同的类型，但一个的成员数量与另一个的成员数量完全相同，并且可以简单地定义一个函数从一个开始对另一个，或另一个对一个。 (并不是说只有一种这样的同构——关键是，你可以选择一种。)

这不是一个好方法。它基本上适用于有限集，但它为无限集引入了不幸的副作用，例如 Add Int Int === Int。尽管如此，对于类型的加法和乘法的基本描述，它似乎还是有用的。