在《用类型思考》一书中，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|？
我很困惑。感谢您的任何提示！
在存在多态类型的情况下，基数无法真正定义。现在人们理解，多态类型"不是人们最初认为的集合"。雷诺兹在他的论文"多态性不是集合论"中提出了一个著名的开创性论点，证明我们不能简单地以"琐碎"的方式解释带有集合的类型并获得有意义的概念。
事实上，在集合中，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)，这在集合中没有意义，正是因为它们不能具有相同的基数。
(即使没有递归类型，在存在多态性的情况下，也可以通过编码获得上述Tforall a. (F a -> a) -> a。
无论如何，为了解决这个僵局，我们需要将a -> Bool解释为函数集以外的其他东西2^a.一个可能的解决方案是使用Scott-连续函数，就像 Scott 所做的那样。一个相关的解决方案是使用稳定函数(参见Girard的"证明和类型"一书(，如果我没记错的话(它使T和T -> Bool的解释具有相同的基数(除非两者都是有限的(。
因此，在存在多态类型的情况下，基数不是用于检查类型同构的正确工具。我们真的需要看看是否有可能制作同构函数及其逆函数，就像你在问题中发布的那样。
基数参数不适用于多态类型(参见@chi的答案(。
但同构本身可以直观地解释为：
类型forall r. (a -> r) -> r的意思是">如果你给我一个将a转换为r的函数，我可以给你一个r。哦，我可以为任何可能r做到这一点">
实现这种承诺的唯一方法就是偷偷地把a拿在手里。
因为我承诺为任何可能r这样做，这意味着我对r本身一无所知，包括如何构建它的值。我唯一可用的就是你给我的功能a -> r。调用此类函数的唯一方法是给它一个a。
这意味着，如果我做出这样的承诺，我一定已经在背后偷偷地a了。
对于更正式的解释，请记住，"同构"在简单意义上意味着"可以毫不含糊地来回转换而不会造成损失"。这就是基数论证所要表达的：如果你有相同数量的东西，你总是可以在它们之间安排配对。
在您的问题中，您已经显示了两种转换：cont转换一种方式，unCont转换另一种方式。你可以微不足道地展示cont . unCont = unCont . cont = id.因此，类型是同构的。
虽然显示这两种转换的存在更为正式，但我发现对这两种类型如何真正"有点同一件事"的直觉并不总是令人满意的，因此我上面给出了直观的解释。