[Haskell-cafe] Solved but strange error in type inference

[AUGER Cédric]

Le Wed, 4 Jan 2012 14:41:21 +0100,
Yves Parès <limestrael at gmail.com> a écrit :

> > I expected the type of 'x' to be universally quantified, and thus
> > can be unified with 'forall a. a' with no problem
> 
> As I get it. 'x' is not universally quantified. f is. [1]
> x would be universally quantified if the type of f was :
> 
> f :: (forall a. a) -> (forall a. a)
> 
> [1] Yet here I'm not sure this sentence is correct. Some heads-up
> from a type expert would be good.
> 

For the type terminology (for Haskell),

notations:
a Q∀ t := a universally quantified in t
a Q∃ t := a existentially quantified in t
a Q∀∃ t := a universally (resp. existentially) quantified in t
a Q∃∀ t := a existentially (resp. universally) quantified in t

Two different names are expected to denote two different type variables.
A type variable is not expected to be many times quantified (else, it
would be meaningless, a way to omit this hypothesis is to think of path
to quantification instead of variable name; to clarify what I mean,
consider the following expression:

forall a. (forall a. a) -> a

we cannot tell what "a is existentially quantified" means, since we
have two a's; but if we rename them into

forall a. (forall b. b) -> a
or
forall b. (forall a. a) -> b

, the meaning is clear; in the following, I expect to always be in a
place where it is clear.)

rules:
(1)   ⊤    ⇒ a Q∀ forall a. t
(2)b Q∀∃ t ⇒ b Q∀∃ forall a. t
(3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above,
                        since "->" is an non binding forall in
                        type theory)
(4)a Q∀∃ t ⇒ a Q∃∀ t -> u

So in this context, we cannot say that 'x' is universally or
existentially quantified, but that the 'type of x' is universally or
existentially quantified 'in' some type (assuming that the type of x
is a type variable).

so:

a Q∃ (forall a. a -> a) -> forall b. b -> b
 since (4) and "a Q∀ forall a. a -> a" due to (1)

and

b Q∀ (forall a. a -> a) -> forall b. b -> b
 since (3) and "b Q∀ forall b. b -> b" due to (1)

The quick way to tell is count the number of unmatched opening
parenthesis before the quantifying forall (assuming you don't put
needless parenthesis) if it is even, you are universally quantified, if
it is odd, you are existentially quantified.

So in:

f :: (forall a. a -> a) -> forall b. b -> b
f id x = id x

the type of 'x' (b) is universally quantified in the type of f,
and the type of 'id' contains an existential quantification in the type
of f (a).

In:

f :: forall a. (a -> a) -> a -> a
f id x = id x

the type of 'x' (a) is universally quantified in the type of f;
there is no existential quantification.

f :: forall a. (forall b. b -> b) -> a -> a
f id x = id x

is very similar to the first case, x is still universally quantified (a)
and there is an existential quantification in id (b).

I guess that the only difference is that when you do a
"f id" in the last case, you might get an error as the program needs to
know the "a" type before applying "id" (of course if there is some use
later in the same function, then the type can be inferred)

Hope that I didn't write wrong things, and if so that you can tell now
for sure if a type is universally or existentially quantified.