Is it valid to lift positive positive forall quantifiers to the outside?

Question

This question came up in discussion on #haskell.

Is it always correct to lift a deeply nested forall to the top, if its occurrence is positive?

E.g:

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

(where P, S, T are to be understood as metavariables) to

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

(which we would normally write just as (P(a) -> S) -> T

I know that you're certainly allowed to collect foralls from some positive positions, such as to the right of the last -> and so on.

This is valid in classical logic so it's not an absurd idea, but in general it's invalid in intuitionistic logic. However my informal game theory intuition of quantifiers which is that each type variable is "chosen by the caller" or "chosen by the callee" suggest that there are really only two choices and you can lift all the "chosen by the caller" options to the top. Unless the interleave of the moves in the game matters?

Answer 1

Assume

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

and let for the sake of this discussion S = (P Int, P Char). A possible type-correct call could then be:

foo (\x :: (forall a. P a) -> (x,x))

Now, assume

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

where S is as above. It is now hard to invoke bar! Let's try to call it on a = Int:

bar (\x :: P Int -> (x, something))

Now we need a something :: P Char which can not simply derived from x. The same happens if a = Char. If a is something else than Int, Char, then it would be even worse.

You mentioned intuitionistic logic. You might see that in that logic the type of foo is stronger than the one of bar. As a stronger hypothesis, the type of foo can therefore be applied to more cases in proofs. So, it shouldn't be a surprise to find that, as a term, foo is applicable in more contexts! :)