问询：System F中Haskell幂集类型Power的可表示性

Haskell支持以下两种类型的定义：

data PowerPower = PP ((PowerPower -> Bool) -> Bool)
data Power = P (Power -> Bool)

PowerPower类型被大量用于驳斥System F集合语义的Reynolds论文中，它在System F中的对应表示如下：

PowerPower = forall A, (((A -> Bool) -> Bool) -> A) -> A
PP = \ z A f -> f (\ u -> z (\ x -> u (x A f)))

Reynolds的驳斥最终论证了PowerPower与自身的双重幂集同构，这与基数相关的康托尔定理相矛盾。两层嵌套幂集对应PowerPower定义中指向Bool的两个箭头。

若使用Power类型替代PowerPower，该驳斥过程将大幅简化：仅需一层幂集即可应用康托尔定理。由此引申出核心问题：我们能否在System F中表示Power类型？该问题存在较高难度，因为Power的底层类型函子\X -> (X -> Bool)为逆变而非协变。由于Haskell支持Power的定义，我们或可基于其在Haskell内存模型中的表示推导对应的System F类型。

内容的提问来源于stack exchange，提问作者V. Semeria