将积极的积极量词提升到外面是否有效？

Question

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

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

例如:

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

(其中P,S,T应理解为metavariables)

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

(我们通常会写作 (P(a) -> S) -> T

我知道你肯定被允许从一些积极的位置收集foralls,例如在最后的右边->等等.

这在经典逻辑中是有效的,因此这不是一个荒谬的想法,但总的来说它在直觉逻辑中是无效的.然而,我的非正式博弈论量词的直觉,即每个类型变量"由来电者选择"或"由被叫者选择"表明实际上只有两个选择,你可以将所有"被来电者选择"选项提升到顶端.除非游戏中的移动交错很重要？

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因此，发现“这个术语”适用于更多上下文也就不足为奇了！:)