haskell - 如何理解类型 a 和 forall r。 (a -> r) -> r 是同构的

Question

在书中 Thinking with Types , 6.4 Continuation Monad 告诉我们 a 和 forall r. (a -> r) -> r 类型是同构的，这可以通过以下函数来证明:

cont :: a -> (forall r. (a -> r) -> r)
cont x = \f -> f x

unCont :: (forall r. (a -> r) -> r) -> a
unCont f = f id

在本书中，它告诉 任何两种具有相同基数的类型将始终彼此同构。 所以我试图找出 a 和 forall r. (a -> r) -> r 类型的基数。

假设 a 类型的基数是 |a| 。那么对于 forall r. (a -> r) -> r 类型，如何计算出它的基数等于 |a| 呢？函数类型 a -> b 的基数为 |b|^|a| ，即 |b| 的 |a| 的幂，因此 forall r. (a -> r) -> r 的基数为 |r|^(|r|^|a|) 。它怎么可能等于 |a| ？

我很困惑。感谢您的任何提示!

Answer 1

在存在多态类型的情况下，基数不能真正定义。现在可以理解，多态类型“不是集合”，正如人们最初所想的那样。雷诺兹在他的论文“多态性不是集合论”中提供了一个著名的开创性论点，证明我们不能简单地以“琐碎”的方式解释带有集合的类型并获得有意义的概念。

确实，成套2^K和 K是不同的红衣主教，第一个更大。同样，2^(2^K)大于 K .然而，F X = 2^(2^X) (类似于 F a = (a -> Bool) -> Bool )形成一个(协变)仿函数，我们可以找到一个不动点

newtype T = T ((T -> Bool) -> Bool)

获取 T与 2^(2^T) 同构，这在集合中没有意义，正是因为它们不能具有相同的基数。

(上面的类型 T 即使没有递归类型，在存在多态性的情况下，也可以通过编码为 forall a. (F a -> a) -> a 来获得。)

无论如何，为了解决这个僵局，我们需要解释 a -> Bool作为函数集以外的东西 2^a .一种可能的解决方案是使用 Scott 连续函数，正如 Scott 所做的那样。一个相关的解决方案是使用稳定函数(参见 Girard 的“证明和类型”一书)，它(如果我没记错的话)解释了 T和 T -> Bool具有相同的基数(除非两者都是有限的)。

因此，基数不是用于在存在多态类型时检查类型同构的正确工具。我们真的需要看看是否可以制作同构函数及其逆函数，就像您在问题中发布的那样。