这个问题在 #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))
现在我们需要一个不能简单地从x得出的something :: P Char。如果a = Char .如果a不是Int, Char，那就更糟了。
你提到了直觉逻辑。您可能会看到，在该逻辑中，foo的类型比bar的类型更强。作为一个更强的假设，foo的类型因此可以应用于证明中的更多情况。因此，发现作为一个术语，foo适用于更多上下文也就不足为奇了！:)