11

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?

drquicksilver
  • 1,627
  • 9
  • 12
  • There's a difference in game theory. With lifted quantifiers you have the choices upfront. With nested quantifiers you will have more information when you make the choice for the inner quantifiers. – augustss Feb 28 '14 at 14:19
  • Right, but that doesn't stop you lifting them to the top. Doesn't it just mean you have a sequence of alternating quantifiers at the top, in general? ∀a,b ∃c,d ∀e,f etc. – drquicksilver Feb 28 '14 at 14:27

1 Answers1

3

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! :)

chi
  • 111,837
  • 3
  • 133
  • 218
  • Well, `P` is an actual, fixed type-term with a free variable `a`. Unless `P Int` and `P Char` are both uninhabited, then just pick inhabitants of them (`pi` and `pc`, say) and call `bar` by passing in `const (pi,pc)`. `bar` seems just as callable as `foo`? Nothing requires me to pass a function to `bar` which inspects its argument. – drquicksilver Feb 28 '14 at 19:47
  • If you have known inhabitants for `S`, I agree. However, in the general case, you can not inhabit `S` without relying on the hypothesis `forall a. P a`. Also, consider the case `P a = Q b a` and as before `S=(P Int, P Char)`. Here `S` could be inhabited only for some values of `b`, yet you can call `foo` without relying on `S` being inhabited. – chi Feb 28 '14 at 21:03