haskell - 将正向的所有量词提升到外部是否有效？

Question

这个问题出现在#haskell 的讨论中。

如果它的出现是积极的，那么将深层嵌套的 forall 提升到顶部是否总是正确的？

例如:

((forall a. P(a)) -> S) -> T

(其中 P、S、T 应理解为元变量)

forall a. (P(a) -> S) -> T

(我们通常写成 (P(a) -> S) -> T
我知道你当然可以从一些积极的位置收集foralls，比如最后一个 ->的右边。等等。

这在经典逻辑中是有效的，所以它不是一个 absurd 的想法，但总的来说它在直觉逻辑中是无效的。然而，我对量词的非正式博弈论直觉是每个类型变量都是“由调用者选择”或“由被调用者选择”，这表明实际上只有两种选择，您可以将所有“由调用者选择”选项提升到顶端。除非游戏中 Action 的交错很重要？

Answer 1

认为

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 的类型比 bar 之一强.作为一个更强的假设， foo 的类型因此在证明中可以应用到更多的案例中。因此，发现作为一个术语， foo 应该不足为奇。适用于更多场景! :)