我正在阅读此博客: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 类型系统有意义吗?
最佳答案
为了不“提及范畴论或高等数学”,作者绕开的术语是基数。他将两种类型定义为 ===
- 如果它们具有相同的基数,则它们彼此相等——也就是说,如果一种类型的可能值与另一种的可能值一样多。
因为如果两个类型具有相等的基数,则它们之间存在同构。 Mul () Bool
可能是与 Bool
不同的类型,但一个的成员数量与另一个的成员数量完全相同,并且可以简单地定义一个函数从一个开始对另一个,或另一个对一个。 (并不是说只有一种这样的同构——关键是,你可以选择一种。)
这不是一个好方法。它基本上适用于有限集,但它为无限集引入了不幸的副作用,例如 Add Int Int === Int
。尽管如此,对于类型的加法和乘法的基本描述,它似乎还是有用的。
关于haskell - 为什么在代数数据类型中,如果我可以为两种类型定义一个特殊的 `from` 和 `to` 函数,这两种类型就可以认为是相等的?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25104709/