如何理解类型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-continuous functions，如Scott所做的那样。一个相关的解决方案是使用stable functions（请参阅Girard的“证明和类型”一书），该书（如果我没记错的话）使T和T -> Bool的解释具有same基数（除非两者都是有限的。

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

Answer 2

基数参数实际上不适用于多态类型（请参阅@chi的答案）。

但是同构本身可以这样直观地解释：

类型forall r. (a -> r) -> r的意思是<< [如果您给我一个将a转换为r的函数，我可以给您返回r。哦，我可以对任何可能的r执行此操作无论如何“

实现这种承诺的唯一方法是秘密地握着a。

由于我承诺将对所有可能的r执行此操作，这意味着我对r本身一无所知，包括如何构造其值。我唯一可以使用的就是您给我的功能a -> r。调用此函数的唯一方法是给它一个a。

这意味着，如果我做出这样的承诺，我必须已经秘密地背着一个a。

---

[作更正式的解释，请记住，“同构”一词的简单含义是“可以明确地来回转换而不会造成损失”。这就是基数参数的含义：如果您拥有相同数量的事物，则始终可以在它们之间进行配对。

并且在您的问题中，您已经显示了两种转换：cont转换一种方式，unCont转换另一种方式。您可以简单地显示cont . unCont = unCont . cont = id。因此，类型是同构的。

虽然显示这两种转换的存在较为正式，但我发现对这两种类型确实是真正的“同一个东西”的直觉并不总是令人满意，因此我在上面给出了直观的解释。