这个问题出现在#haskell 的讨论中。
如果它的出现是积极的，那么将深层嵌套的 forall 提升到顶部是否总是正确的？
例如：
((forall a. P(a)) -> S) -> T
（其中 P、S、T 应理解为元变量）
forall a. (P(a) -> S) -> T
（我们通常会写成(P(a) -> S) -> T
我知道你当然可以从一些积极的位置收集foralls，比如在最后的右边->等等。
这在经典逻辑中是有效的，所以它不是一个荒谬的想法，但总的来说它在直觉逻辑中是无效的。然而，我对量词的非正式博弈论直觉，即每个类型变量都是“由调用者选择”或“由被调用者选择”表明实际上只有两种选择，您可以将所有“由调用者选择”选项提升到顶端。除非游戏中动作的交错很重要？
认为
foo :: ((forall a. P a) -> S) -> T
为了这个讨论，让我们S = (P Int, P Char)。一个可能的类型正确调用可能是：
foo (\x :: (forall a. P a) -> (x,x))
现在，假设
bar :: forall a. (P a -> S) -> T
S如上。现在很难调用bar！让我们尝试调用它a = Int：
bar (\x :: P Int -> (x, something))
现在我们需要一个something :: P Char不能简单地从x. 如果 .也会发生同样的情况a = Char。如果a不是Int, Char，那就更糟了。
你提到了直觉主义逻辑。您可能会看到，在该逻辑中，类型foo比 of 更强bar。作为一个更强的假设，foo因此可以将 的类型应用于证明中的更多案例。foo因此，发现它作为一个术语适用于更多情况也就不足为奇了！:)